VMC: recent advances and challenges ahead

The variability model checker VMC accepts a product family specified as a Modal Transition System (MTS) with additional variability constraints. Consequently, it offers behavioral variability analyses over both the family and its valid product behavior. This ranges from product derivation and simulation to efficient on-the-fly model checking of logical properties expressed in a variability-aware version of action-based CTL. In this paper, we first explain the reasons and assumptions underlying the choice for a modeling and analysis framework based on MTSs. Subsequently, we present recent advances on proving inheritance of behavioral analysis properties from a product family to its valid products. Finally, we illustrate challenges remaining for the future.