Modelling and Model Checking Software Product Lines

In product line engineering, systems are developed in families and differences
between family members are expressed in terms of features.  We study the problem
of model checking product line behaviours against temporal properties. This is
more difficult than for single systems because a product line with n features
yields up to 2^n individual systems to verify. As each individual verification
suffers from state explosion, it is crucial to have efficient formalisms and
heuristics.

First, we propose featured transition systems, a semantic model that describes
the combined behaviour of an entire system family. We then define a model
checking algorithm that allows to verify featured transition systems against
temporal properties. When it succeeds, all systems of the family satisfy the
property. Otherwise, the algorithm pinpoints those that do not.

Second, we discuss two implementations of featured transition systems. A first
uses a symbolic representation of the state space and is implemented as part of
the NuSMV model checker.  The second, SNIP, uses a semi-symbolic on-the-fly
algorithm.  SNIP comes with an intuitive specification language based on
Promela.  Benchmarks show that our algorithms outperform classical model
checking algorithms executed over each system of the family separately.