TY - GEN
T1 - Family-Based SPL model checking using parity games with variability
AU - ter Beek, Maurice H.
AU - van Loo, Sjef
AU - de Vink, Erik P.
AU - Willemse, Tim A.C.
PY - 2020
Y1 - 2020
N2 - 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 μ-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 the modal μ-calculus 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 the product-based method of solving the standard parity games obtained by projection with classical algorithms.
AB - 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 μ-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 the modal μ-calculus 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 the product-based method of solving the standard parity games obtained by projection with classical algorithms.
UR - http://www.scopus.com/inward/record.url?scp=85084262875&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-45234-6_12
DO - 10.1007/978-3-030-45234-6_12
M3 - Conference contribution
AN - SCOPUS:85084262875
SN - 9783030452339
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 245
EP - 265
BT - Fundamental Approaches to Software Engineering- 23rd International Conference, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings
A2 - Wehrheim, Heike
A2 - Cabot, Jordi
PB - Springer Gabler
T2 - 23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Y2 - 25 April 2020 through 30 April 2020
ER -