Family-based model checking of fMultiLTL properties

LTL; Model Checking; Software Product Lines; Temporal Multi-Properties; Feature expression; Model checker; Model-checking algorithms; Models checking; Property; Software Product Line; System families; Temporal multi-property; Human-Computer Interaction; Computer Networks and Communications; Computer Vision and Pattern Recognition; Software

Abstract :

[en] We introduce a new logic for expressing multi-properties of system families (Software Product Lines - SPLs). While the standard LTL logic refers only to a single trace at a time, fMultiLTL logic proposed here refers to multiple traces originating from different sets of variants of the SPL. This is achieved by allowing so-called featured quantification over traces, ∀ψ and ∃ψ, where the feature expression ψ describes a set of variants (sub-family) the quantified trace comes from. A specialized family-based model checking algorithm for verifying some fragments of fMultiLTL is given. A prototype family-based model checker, called Dądalux, has been implemented. We illustrate the practicality of this approach on several interesting SPL models.

Disciplines :

Computer science

Author, co-author :

Dimovski, Aleksandar S. ; Mother Teresa University, Skopje, North Macedonia

LAZREG, Sami ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SerVal

CORDY, Maxime ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SerVal

Legay, Axel ; Université Catholique de Louvain, Belgium

External co-authors :

yes

Language :

English

Title :

Family-based model checking of fMultiLTL properties

Publication date :

28 August 2023

Event name :

Proceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A

Event place :

Tokyo, Jpn

Event date :

28-08-2023 => 01-09-2023

Audience :

International

Main work title :

27th ACM International Systems and Software Product Line Conference, SPLC 2023 - Proceedings

Editor :

Arcaini, Paolo

Publisher :

Association for Computing Machinery

ISBN/EAN :

9798400700910

Peer reviewed :

Peer reviewed

Additional URL :

https://dl.acm.org/doi/pdf/10.1145/3579027.3608976

Funders :

Association for Computing Machinery
HITACHI - Inspire the Next
pure systems

Funding text :

Maxime Cordy and Sami Lazreg are supported by FNR Luxembourg (grants C19/IS/13566661/BEEHIVE/Cordy and INTER/FNRS/20/15-077233/Scaling Up Variability/Cordy). Axel Legay is supported by FNRS Belgium (grant PDR/PDN - T013721).

Available on ORBilu :

since 15 December 2023

Statistics

Number of views

24 (1 by Unilu)

Number of downloads

20 (1 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

Bibliography

Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. 2011. Detection of feature interactions using feature-aware verification. In 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011). 372-375. https: //doi. org/10. 1109/ASE. 2011. 6100075
Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press.
Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. 2004. Secure Information Flow by Self-Composition. In 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004). IEEE Computer Society, 100-114. https: //doi. org/10. 1109/CSFW. 2004. 17
Eric Bodden, Társis Tolêdo, Márcio Ribeiro, Claus Brabrand, Paulo Borba, and Mira Mezini. 2013. SPLLIFT: Statically analyzing software product lines in minutes instead of years. In ACM SIGPLAN Conference on PLDI '13. 355-364.
Milan Ceska, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. 2019. Model Repair Revamped: On the Automated Synthesis of Markov Chains. In Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday (LNCS, Vol. 11500). Springer, 107-125. https: //doi. org/10. 1007/978-3-030-31514-6_7
Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz, and Christel Baier. 2018. ProFeat: Feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput. 30, 1 (2018), 45-75. https: //doi. org/10. 1007/s00165-017-0432-4
Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. 2014. Temporal Logics for Hyperproperties. In Principles of Security and Trust-Third International Conference, POST 2014, Proceedings (LNCS, Vol. 8414). Springer, 265-284. https: //doi. org/10. 1007/978-3-642-54792-8_15
Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur. 18, 6 (2010), 1157-1210. https: //doi. org/10. 3233/JCS-2009-0393
Andreas Classen, Quentin Boucher, and Patrick Heymans. 2011. A text-based approach to feature modelling: Syntax and semantics of TVL. Sci. Comput. Program. 76, 12 (2011), 1130-1143. https: //doi. org/10. 1016/j. scico. 2010. 10. 005
Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, and Pierre-Yves Schobbens. 2012. Model checking software product lines with SNIP. STTT 14, 5 (2012), 589-612. https: //doi. org/10. 1007/s10009-012-0234-1
Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, and Jean-François Raskin. 2013. Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Software Eng. 39, 8 (2013), 1069-1089. https: //doi. org/10. 1109/TSE. 2012. 86
Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, and Jean-François Raskin. 2013. Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Software Eng. 39, 8 (2013), 1069-1089. https: //doi. org/10. 1109/TSE. 2012. 86
Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay, and Jean-François Raskin. 2010. Model checking lots of systems: Efficient verification of temporal properties in software product lines. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1, ICSE 2010. ACM, 335-344. https: //doi. org/10. 1145/1806799. 1806850
Paul Clements and Linda Northrop. 2001. Software Product Lines: Practices and Patterns. Addison-Wesley.
Maxime Cordy, Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, and Axel Legay. 2013. ProVeLines: A product line of verifiers for software product lines. In 17th International Software Product Line Conference co-located workshops, SPLC 2013 workshops. ACM, 141-146. https: //doi. org/10. 1145/2499777. 2499781
Maxime Cordy, Patrick Heymans, Axel Legay, Pierre-Yves Schobbens, Bruno Dawagne, and Martin Leucker. 2014. Counterexample guided abstraction refinement of product-line behavioural models. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22). 190-201. https: //doi. org/10. 1145/2635868. 2635919
Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, and Axel Legay. 2013. Beyond boolean product-line model checking: Dealing with feature attributes and multi-features. In 35th International Conference on Software Engineering, ICSE '13. IEEE Computer Society, 472-481. https: //doi. org/10. 1109/ICSE. 2013. 6606593
Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008. Proceedings (LNCS, Vol. 4963), C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer, 337-340. https: //doi. org/10. 1007/978-3-540-78800-3_24
Aleksandar S. Dimovski. 2016. Symbolic Game Semantics for Model Checking Program Families. In Model Checking Software-23nd International Symposium, SPIN 2016, Proceedings (LNCS, Vol. 9641). Springer, 19-37.
Aleksandar S. Dimovski. 2018. Abstract Family-based Model Checking using Modal Featured Transition Systems: Preservation of CTL?. In Fundamental Approaches to Software Engineering-21st International Conference, FASE 2018, Proceedings (LNCS, Vol. 10802). Springer, 301-318.
Aleksandar S. Dimovski. 2018. Verifying annotated program families using symbolic game semantics. Theor. Comput. Sci. 706 (2018), 35-53. https: //doi. org/ 10. 1016/j. Tcs. 2017. 09. 029
Aleksandar S. Dimovski. 2020. {CTL} family-based model checking using variability abstractions and modal transition systems. STTT 22, 1 (2020), 35-55. https: //doi. org/10. 1007/s10009-019-00528-0
Aleksandar S. Dimovski. 2021. Lifted termination analysis by abstract interpretation and its applications. In GPCE '21: Concepts and Experiences, 2021. ACM, 96-109. https: //doi. org/10. 1145/3486609. 3487202
Aleksandar S. Dimovski. 2022. Model sketching by abstraction refinement for lifted model checking. In SAC '22: The 37th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, 2022. ACM, 1845-1848. https: //doi. org/10. 1145/3477314. 3507170
Aleksandar S. Dimovski. 2023. Quantitative program sketching using decision tree-based lifted analysis. J. Comput. Lang. 75 (2023), 101206. https: //doi. org/10. 1016/j. cola. 2023. 101206
Aleksandar S. Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, and Andrzej Wasowski. 2016. Efficient family-based model checking via variability abstractions. STTT (2016). https: //doi. org/10. 1007/s10009-016-0425-2
Aleksandar S. Dimovski and Sven Apel. 2021. Lifted Static Analysis of Dynamic Program Families by Abstract Interpretation. In 35th European Conference on Object-Oriented Programming, ECOOP 2021 (LIPIcs, Vol. 194). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 14: 1-14: 28. https: //doi. org/10. 4230/LIPIcs. ECOOP. 2021. 14
Aleksandar S. Dimovski, Sven Apel, and Axel Legay. 2022. Several lifted abstract domains for static analysis of numerical program families. Sci. Comput. Program. 213 (2022), 102725. https: //doi. org/10. 1016/j. scico. 2021. 102725
Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. 2015. Variability Abstractions: Trading Precision for Speed in Family-Based Analyses. In 29th European Conference on Object-Oriented Programming, ECOOP 2015 (LIPIcs, Vol. 37). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 247-270. https: //doi. org/10. 4230/LIPIcs. ECOOP. 2015. 247
Aleksandar S. Dimovski, Claus Brabrand, and AndrzejWasowski. 2018. Variability abstractions for lifted analysis. Sci. Comput. Program. 159 (2018), 1-27.
Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. 2019. Finding suitable variability abstractions for lifted analysis. Formal Aspects Comput. 31, 2 (2019), 231-259. https: //doi. org/10. 1007/s00165-019-00479-y
Aleksandar S. Dimovski, Axel Legay, and Andrzej Wasowski. 2020. Generalized abstraction-refinement for game-based CTL lifted model checking. Theor. Comput. Sci. 837 (2020), 181-206. https: //doi. org/10. 1016/j. Tcs. 2020. 06. 011
Aleksandar S. Dimovski and Andrzej Wasowski. 2017. From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL. In Models, Algorithms, Logics and Tools-Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday (LNCS, Vol. 10460). Springer, 249-268. https: //doi. org/10. 1007/978-3-319-63121-9_13
Aleksandar S. Dimovski and AndrzejWasowski. 2017. Variability-specific Abstraction Refinement for Family-Based Model Checking. In Fundamental Approaches to Software Engineering-20th International Conference, FASE 2017, Proceedings (LNCS, Vol. 10202). 406-423. https: //doi. org/10. 1007/978-3-662-54494-5_24
Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. 2015. Algorithms for Model Checking HyperLTL and HyperCTL. In Computer Aided Verification-27th International Conference, CAV 2015, Proceedings, Part I (LNCS, Vol. 9206). Springer, 30-48. https: //doi. org/10. 1007/978-3-319-21690-4_3
Paul Gazzillo and Robert Grimm. 2012. SuperC: Parsing all of C by taming the preprocessor. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, Beijing, China-June 11-16, 2012, Jan Vitek, Haibo Lin, and Frank Tip (Eds.). ACM, 323-334. https: //doi. org/10. 1145/2254064. 2254103
Ohad Goudsmid, Orna Grumberg, and Sarai Sheinvald. 2021. Compositional Model Checking for Multi-properties. In Verification, Model Checking, and Abstract Interpretation-22nd International Conference, VMCAI 2021, Proceedings (LNCS, Vol. 12597). Springer, 55-80. https: //doi. org/10. 1007/978-3-030-67067-2_4
Gerard J. Holzmann. 2004. The SPIN Model Checker-primer and reference manual. Addison-Wesley.
Alexandru F. Iosif-Lazar, Jean Melo, Aleksandar S. Dimovski, Claus Brabrand, and AndrzejWasowski. 2017. Effective Analysis of C Programs by Rewriting Variability. Programming Journal 1, 1 (2017), 1. https: //doi. org/10. 22152/programmingjournal. org/2017/1/1
Christian Kästner, Sven Apel, Thomas Thüm, and Gunter Saake. 2012. Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21, 3 (2012), 14.
Christian Kästner, Paolo G. Giarrusso, Tillmann Rendel, Sebastian Erdweg, Klaus Ostermann, and Thorsten Berger. 2011. Variability-aware parsing in the presence of lexical macros and conditional compilation. In Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011. 805-824. https: //doi. org/ 10. 1145/2048066. 2048128
Jeff Kramer, Jeff Magee, Morris Sloman, and A. Lister. 1983. CONIC: An Integrated Approach to Distributed Computer Control Systems. IEE Proc. 130, 1 (1983), 1-10.
Kenneth L. McMillan. 2003. Craig Interpolation and Reachability Analysis. In Static Analysis, 10th International Symposium, SAS 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2694). Springer, 336. https: //doi. org/10. 1007/3-540-44898-5_18
Klaus Pohl, Günter Böckle, and Frank van der Linden. 2005. Software Product Line Engineering: Foundations, Principles and Techniques. Springer.
Riccardo Pucella and Fred B. Schneider. 2006. Independence From Obfuscation: A Semantic Framework for Dive. In 19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006). IEEE Computer Society, 230-241. https: //doi. org/10. 1109/CSFW. 2006. 15
Fabio Somenzi and Aaron R. Bradley. 2011. IC3: Where monolithic and incremental meet. In International Conference on Formal Methods in Computer-Aided Design, FMCAD '11. FMCAD Inc., 3-8. http: //dl. Acm. org/citation. cfm?id=2157657
Maurice H. Ter Beek, Erik P. de Vink, and Tim A. C. Willemse. 2017. Family-Based Model Checking with mCRL2. In Fundamental Approaches to Software Engineering-20th International Conference, FASE 2017, Proceedings (LNCS, Vol. 10202). 387-405. https: //doi. org/10. 1007/978-3-662-54494-5_23
Maurice H. Ter Beek, Alessandro Fantechi, Stefania Gnesi, and Franco Mazzanti. 2016. Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints. J. Log. Algebr. Meth. Program. 85, 2 (2016), 287-315. https: //doi. org/10. 1016/j. jlamp. 2015. 09. 004
Tachio Terauchi and Alexander Aiken. 2005. Secure Information Flow as a Safety Problem. In Static Analysis, 12th International Symposium, SAS 2005, Proceedings (LNCS, Vol. 3672), Chris Hankin and Igor Siveroni (Eds.). Springer, 352-367. https: //doi. org/10. 1007/11547662_24
Moshe Y. Vardi and Pierre Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification. In Proceedings of the Symposium on Logic in Computer Science (LICS '86). IEEE Computer Society, 332-344.
Alexander von Rhein, Jörg Liebig, Andreas Janker, Christian Kästner, and Sven Apel. 2018. Variability-Aware Static Analysis at Scale: An Empirical Study. ACM Trans. Softw. Eng. Methodol. 27, 4 (2018), 18: 1-18: 33. https: //doi. org/10. 1145/ 3280986
Alexander von Rhein, Thomas Thüm, Ina Schaefer, Jörg Liebig, and Sven Apel. 2016. Variability encoding: From compile-time to load-time variability. J. Log. Algebr. Meth. Program. 85, 1 (2016), 125-145. https: //doi. org/10. 1016/j. jlamp. 2015. 06. 007