Abstract
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.
Chapter PDF
Similar content being viewed by others
References
A. Classen, P. Heymans, and P.-Y. Schobbens. What’s in a Feature: A Requirements Engineering Perspective. In J.L. Fiadeiro and P. Inverardi, editors, FASE’08, volume 4961 of LNCS, pages 16–30. Springer, 2008.
S. Apel, D. Batory, C. Kästner, and G. Saake. Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, 2013.
A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin. Model Checking \(\underline{\text{Lots}}\) of Systems: Efficient Verification of Temporal Properties in Software Product Lines. In Proc. ICSE’10, pages 335–344. ACM, 2010.
A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. Raskin. Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and their Application to LTL Model Checking. IEEE Trans. Softw. Eng., 39(8):1069–1089, 2013.
M. Cordy, X. Devroey, A. Legay, G. Perrouin, A. Classen, P. Heymans, P.-Y. Schobbens, and J.-F. Raskin. A Decade of Featured Transition Systems. In M.H. ter Beek, A. Fantechi, and L. Semini, editors, From Software Engineering to Formal Methods and Tools, and Back, volume 11865 of LNCS, pages 285–312. Springer, 2019.
T. Thüm, S. Apel, C. Kästner, I. Schaefer, and G. Saake. A Classification and Survey of Analysis Strategies for Software Product Lines. ACM Comput. Surv., 47(1):6:1–6:45, 2014.
A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transf., 14(5):589–612, 2012.
M. Cordy, A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. ProVeLines: a product line of verifiers for software product lines. In Proc. SPLC’13, volume 2, pages 141–146. ACM, 2013.
M.H. ter Beek, F. Mazzanti, and A. Sulova. VMC: A Tool for Product Variability Analysis. In D. Giannakopoulou and D. Méry, editors, Proc. FM’12, volume 7436 of LNCS, pages 450–454. Springer, 2012.
P. Chrszon, C. Dubslaff, S. Klüppelholz, and C. Baier. Family-Based Modeling and Analysis for Probabilistic Systems – Featuring ProFeat. In P. Stevens and A. Wąsowski, editors, Proc. FASE’16, volume 9633 of LNCS, pages 287–304, 2016.
P. Chrszon, C. Dubslaff, S. Klüppelholz, and C. Baier. ProFeat: feature-oriented engineering for family-based probabilistic model checking. Form. Asp. Comp., 30(1):45–75, 2018.
M.H. ter Beek, A. Legay, A. Lluch Lafuente, and A. Vandin. A framework for quantitative modeling and analysis of highly (re)configurable systems. IEEE Trans. Softw. Eng., 2018.
A. Vandin, M.H. ter Beek, A. Legay, and A. Lluch Lafuente. QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems. In K. Havelund, J. Peleska, B. Roscoe, and E. de Vink, editors, Proc. FM’18, volume 10951 of LNCS, pages 329–337. Springer, 2018.
A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. Symbolic Model Checking of Software Product Lines. In Proc. ICSE’11, pages 321–330. ACM, 2011.
A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program., 80(B):416–439, 2014.
A.S. Dimovski, A.S. Al-Sibahi, C. Brabrand, and A. Wąsowski. Family-Based Model Checking Without a Family-Based Model Checker. In B. Fischer and J. Geldenhuys, editors, Proc. SPIN’15, volume 9232 of LNCS, pages 282–299. Springer, 2015.
M. Lochau, S. Mennicke, H. Baller, and L. Ribbeck. Incremental model checking of delta-oriented software product lines. J. Log. Algebr. Meth. Program., 85(1):245–267, 2016.
M.H. ter Beek and E.P. de Vink. Using mCRL2 for the Analysis of Software Product Lines. In Proc. FormaliSE’14, pages 31–37. IEEE, 2014.
M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. Family-Based Model Checking with mCRL2. In M. Huisman and J. Rubin, editors, Proc. FASE’17, volume 10202 of LNCS, pages 387–405. Springer, 2017.
S. Cranen, J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, E.P. de Vink, W. Wesselink, and T.A.C. Willemse. An Overview of the mCRL2 Toolset and Its Recent Advances. In N. Piterman and S.A. Smolka, editors, Proc. TACAS’13, volume 7795 of LNCS, pages 199–213. Springer, 2013.
O. Bunte, J.F. Groote, J.J.A. Keiren, M. Laveaux, T. Neele, E.P. de Vink, W. Wesselink, A. Wijs, and T.A.C. Willemse. The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability. In T. Vojnar and L. Zhang, editors, Proc. TACAS’19, volume 11428 of LNCS, pages 21–39. Springer, 2019.
M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. Towards a Feature mu-Calculus Targeting SPL Verification. Electr. Proc. Theor. Comput. Sci., 206:61–75, 2016.
A.S. Dimovski. Symbolic Game Semantics for Model Checking Program Families. In D. Bošnački and A. Wijs, editors, Proc. SPIN’16, volume 9641 of LNCS, pages 19–37. Springer, 2016.
A.S. Dimovski and A. Wąsowski. Variability-Specific Abstraction Refinement for Family-Based Model Checking. In M. Huisman and J. Rubin, editors, Proc. FASE’17, volume 10202 of LNCS, pages 406–423. Springer, 2017.
A.S. Dimovski. Abstract Family-Based Model Checking Using Modal Featured Transition Systems: Preservation of CTL\(^*\). In A. Russo and A. Schürr, editors, Proc. FASE’18, volume 10802 of LNCS, pages 301–318. Springer, 2018.
A.S. Dimovski, A. Legay, and A. Wąsowski. Variability Abstraction and Refinement for Game-Based Lifted Model Checking of Full CTL. In R. Hähnle and W. van der Aalst, editors, Proc. FASE’19, volume 11424 of LNCS, pages 192–209. Springer, 2019.
W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135–183, 1998.
O. Friedmann and M. Lange. Solving Parity Games in Practice. In Z. Liu and A.P. Ravn, editors, Proc. ATVA’09, volume 5799 of LNCS, pages 182–196. Springer, 2009.
T. van Dijk. Oink: An Implementation and Evaluation of Modern Parity Game Solvers. In D. Beyer and M. Huisman, editors, Proc. TACAS’18, volume 10805 of LNCS, pages 291–308. Springer, 2018.
J.C. Bradfield and I. Walukiewicz. The mu-calculus and model checking. In E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem, editors, Handbook of Model Checking, chapter 26, pages 871–919. Springer, 2018.
J. Lind-Nielsen. BuDDy: A Binary Decision Diagram package. Technical Report IT-TR 1999–028, IT University of Copenhagen, 1999.
H. Cohen, J. Whaley, J. Wildt, and N. Gorogiannis. BuDDy: A Binary Decision Diagram library. http://sourceforge.net/p/buddy/. Last visited October 18, 2019.
J. Kramer, J. Magee, M. Sloman, and A. Lister. CONIC: an integrated approach to distributed computer control systems. IEE Proc. E, 130(1):1–10, 1983.
X. Devroey, G. Perrouin, M. Papadakis, A. Legay, P.-Y. Schobbens, and P. Heymans. Featured Model-based Mutation Analysis. In Proc. ICSE’16, pages 655–666. ACM, 2016.
A.S. Dimovski, A.S. Al-Sibahi, C. Brabrand, and A. Wąsowski. Efficient family-based model checking via variability abstractions. Int. J. Softw. Tools Technol. Transf., 19(5):585–603, 2017.
M.H. ter Beek, F. Damiani, M. Lienhardt, F. Mazzanti, and L. Paolini. Static Analysis of Featured Transition Systems. In Proc. SPLC’19, pages 39–51. ACM, 2019.
M. Plath and M. Ryan. Feature integration using a feature construct. Sci. Comput. Program., 41(1):53–84, 2001.
A.S. Dimovski. CTL\(^*\) family-based model checking using variability abstractions and modal transition systems. Int. J. Softw. Tools Technol. Transf., 22(1):35–55, 2020.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
ter Beek, M.H., van Loo, S., de Vink, E.P., Willemse, T.A.C. (2020). Family-Based SPL Model Checking Using Parity Games with Variability. In: Wehrheim, H., Cabot, J. (eds) Fundamental Approaches to Software Engineering. FASE 2020. Lecture Notes in Computer Science(), vol 12076. Springer, Cham. https://doi.org/10.1007/978-3-030-45234-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-45234-6_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45233-9
Online ISBN: 978-3-030-45234-6
eBook Packages: Computer ScienceComputer Science (R0)