Family-based model checking of SPL based on mCRL2

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 featureoriented extension of the modal μ-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.