2020
Conference article  Open Access

Family-based SPL model checking using parity games with variability

Ter Beek M. H., Van Loo S., De Vink E. P., Willemse T. A. C.

Variability-intensive systems  Mu-calculus  Article  Model checking  Variability parity games  Software product lines  mCRL2 

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 the modal mu-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.

Source: FASE 2020 - International Conference on Fundamental Approaches to Software Engineering, pp. 245–265, Dublin, Ireland, 25-30/04/2020

Publisher: Springer, Berlin, DEU


Metrics



Back to previous page
BibTeX entry
@inproceedings{oai:it.cnr:prodotti:420348,
	title = {Family-based SPL model checking using parity games with variability},
	author = {Ter Beek M. H. and Van Loo S. and De Vink E. P. and Willemse T. A. C.},
	publisher = {Springer, Berlin, DEU},
	doi = {10.1007/978-3-030-45234-6_12},
	booktitle = {FASE 2020 - International Conference on Fundamental Approaches to Software Engineering, pp. 245–265, Dublin, Ireland, 25-30/04/2020},
	year = {2020}
}