Title of paper: Family-Based SPL Model Checking Using Parity Games with Variability


Family-based SPL model checking concerns the simultaneous verification of multiple product models, aiming to improve on enumerative product-based verification, by capitalising on the common features and behaviour of products in a software product line (SPL), typically modelled as a featured transition system (FTS). We propose efficient family-based SPL model checking of modal mu-calculus formulae on FTSs based on variability parity games, which extend parity games with conditional edges labelled with (feature) configurations, by reducing the SPL model checking problem for modal mu-calculus formulae on FTSs to the variability parity game solving problem, based on an encoding of FTSs as variability parity games. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration sets, outperforms in (nearly) all cases the product-based method of solving standard parity games obtained by projection with classical algorithms.