Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints

• A formal MTS framework to model and analyse variability in product family behaviour.
• A specific MTS refinement relation induces valid product behaviour modelled as LTSs.
• The variability-aware action-based branching-time modal temporal logic v-ACTL.
• Results on property preservation from a MTS to LTSs: from family to product behaviour.
• VMC tool: efficient on-the-fly model checking over family and product behaviour alike.

We present the formal underpinnings of a modelling and analysis framework for the specification and verification of variability in product families. We address variability at the behavioural level by modelling the family behaviour by means of a Modal Transition System (MTS) with an associated set of variability constraints expressed over action labels. An MTS is a Labelled Transition System (LTS) which distinguishes between optional and mandatory transitions. Steered by the variability constraints, the inclusion or exclusion of labelled transitions in an LTS refining the MTS determines the family's possible product behaviour. We formalise this as a special-purpose refinement relation for MTSs, which differs fundamentally from the classical one, and show how to use it for the definition and derivation of valid product behaviour starting from product family behaviour. We also present a variability-aware action-based branching-time modal temporal logic to express properties over MTSs, and demonstrate a number of results regarding the preservation of logical properties from family to product behaviour. These results pave the way for the more efficient family-based analyses of MTSs, limiting the need for product-by-product analyses of LTSs. Finally, we define a high-level modal process algebra for the specification of MTSs. The complete framework is implemented in a model-checking tool: given the behaviour of a product family modelled as an MTS with an additional set of variability constraints, it allows the explicit generation of valid product behaviour as well as the efficient on-the-fly verification of logical properties over family and product behaviour alike.