Family-Based Model Checking of SPL based on mCRL2
Z. Ben Snaiba, E.P. de Vink, and T.A.C. Willemse

We discuss how the general-purpose model checker mCRL2 can be used for
family-based verification of behavioral properties of software product
lines. This is achieved by exploiting a feature-oriented extension of
the modal mu-calculus for the specification of SPL properties, and for
its model checking by encoding it back into the logic of mCRL2. Using
the example of the well-known minepump SPL an illustration of the
possibilities of the approach is given.