Family-Based Model Checking with mCRL2
M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse

Family-based model checking targets the simultaneous verification of multiple
system variants, a technique to handle feature-based variability that is
intrinsic to software product lines (SPLs). We present an approach for
family-based verification based on the feature mu-calculus muLf, which combines
modalities with feature expressions. This logic is interpreted over featured
transition systems, a well-accepted model of SPLs, which allows one to reason
over the collective behavior of a number of variants (a family of products).
Via an embedding into the modal mu-calculus with data, underpinned by the
general-purpose mCRL2 toolset, off-the-shelf tool support for muLf becomes
readily available. We illustrate the feasibility of our approach on an SPL
benchmark model and show the runtime improvement that family-based model
checking with mCRL2 offers with respect to model checking the benchmark
product-by-product.