[en] This paper presents Daedalux, a new model-checking platform for variability-intensive systems based on Featured Transition System theory developed in C++. Daedalux features a modular, flexible, and extensible architecture, overcoming previous tools' maintainability limitations. In addition, during verification, it provides visualizations of intermediate models and results. A key added value of Daedalux lies in its software architecture, which allows straightforward extension and integration of new formalisms and verification algorithms. We have implemented two recent FTS-based approaches, i.e., a statistical model-checking algorithm for LTL properties and an exhaustive algorithm for multi-LTL properties. By reducing the entry barrier of understanding variability-aware model checking and facilitating the comprehension and extension of the software tools, we hope to increase the community's ambitions in developing novel model-checking advances. A video demonstration of Daedalux can be found at https://youtu.be/kirpOAlV-0w.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
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
HANSEN, Simon Thrane ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust > SerVal > Team Maxime CORDY
Legay, Axel ; Université Catholique de Louvain, Belgium
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
Daedalux: An Extensible Platform for Variability-Aware Model Checking
Date de publication/diffusion :
14 avril 2024
Nom de la manifestation :
Proceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings
Lieu de la manifestation :
Lisbon, Prt
Date de la manifestation :
14-04-2024 => 20-04-2024
Titre de l'ouvrage principal :
Proceedings - 2024 ACM/IEEE 46th International Conference on Software Engineering: Companion, ICSE-Companion 2024
Erika Abrahám, Ezio Bartocci, Borzoo Bonakdarpour, and Oyendrila Dobe. 2020. Probabilistic Hyperproperties with Nondeterminism. In Automated Technology for Verification and Analysis-18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12302), Dang Van Hung and Oleg Sokolsky (Eds.). Springer, 518-534. https: //doi.org/10.1007/978-3-030-59152-6-29
Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press, Cambridge, Mass.
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.
Andreas Classen, Quentin Boucher, and Patrick Heymans. 2011. A text-based approach to feature modelling: Syntax and semantics of TVL. SCP 76 (December 2011), 1130-1143. Issue 12.
Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, and Pierre-Yves Schobbens. 2012. Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transf. 14, 5 (2012), 589-612.
Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, and Jean-Francois 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.
Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay, and Jean-Francois Raskin. 2010. Model checking lots of systems: Efficient verification of temporal properties in software product lines. In ICSE 2010, Proceedings, Jeff Kramer, Judith Bishop, Premkumar T. Devanbu, and Sebastián Uchitel (Eds.). ACM, 335-344.
Maxime Cordy, Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, and Axel Legay. 2013. ProVeLines: A product line of verifiers for software product lines. In SPLC. ACM, New York, NY, USA, 141-146.
Maxime Cordy, Xavier Devroey, Axel Legay, Gilles Perrouin, Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, and Jean-Francois Raskin. 2019. A Decade of Featured Transition Systems. In From Software Engineering to Formal Methods and Tools, and Back-Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday (LNCS, Vol. 11865), Maurice H. ter Beek, Alessandro Fantechi, and Laura Semini (Eds.). Springer, 285-312.
Maxime Cordy, Patrick Heymans, Axel Legay, Pierre-Yves Schobbens, Bruno Dawagne, and Martin Leucker. 2016. Counterexample guided abstraction refinement of product-line behavioural models. In Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik, 23.-26. Februar 2016, Wien, Osterreich (LNI, Vol. P-252), Jens Knoop and Uwe Zdun (Eds.). GI, 79-80. https: //dl.gi.de/handle/20.500.12116/732
Maxime Cordy, Sami Lazreg, Mike Papadakis, and Axel Legay. 2021. Statistical model checking for variability-intensive systems: Applications to bug detection and minimization. Formal Aspects of Computing 33 (2021), 1147-1172.
Aleksandar S. Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, and Andrzej Wasowski. 2015. Family-Based Model Checking Without a Family-Based Model Checker. In SPIN 2015, Proceedings (LNCS, Vol. 9232), Bernd Fischer and Jaco Geldenhuys (Eds.). Springer, 282-299.
Aleksandar S. Dimovski, Sami Lazreg, Maxime Cordy, and Axel Legay. 2023. Family-Based Model Checking of FMultiLTL Properties. In SPLC 2023, Proceedings (Tokyo, Japan) (SPLC '23). ACM, New York, NY, USA, 41-51.
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.
Clemens Dubslaff, Christel Baier, and Sascha Klüppelholz. 2015. Probabilistic Model Checking for Feature-Oriented Systems. In Transactions on Aspect-Oriented Software Development XII. Springer, Berlin, Germany, 180-220.
Erich Gamma, Richard Helm, Ralph Johnson, John Vlissides, and Grady Booch. 1994. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional, Boston, MA, USA.
Paul Gastin and Denis Oddoux. 2001. Fast LTL to Büchi Automata Translation. In CAV 2001, Proceedings (LNCS, Vol. 2102), Gérard Berry, Hubert Comon, and Alain Finkel (Eds.). Springer, 53-65.
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, Copenhagen, Denmark, January 17-19, 2021, Proceedings (Lecture Notes in Computer Science, Vol. 12597), Fritz Henglein, Sharon Shoham, and Yakir Vizel (Eds.). Springer, 55-80. https: //doi.org/10.1007/978-3-030-67067-2-4
Holger Hermanns, Björn Wachter, and Lijun Zhang. 2008. Probabilistic CEGAR. In Computer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). 162-175.
Gerard J. Holzmann. 2004. The SPIN Model Checker-primer and reference manual. Addison-Wesley.
Paulius Juodisius, Atrisha Sarkar, Raghava Rao Mukkamala, Michal Antkiewicz, Krzysztof Czarnecki, and AndrzejWasowski. 2019. Clafer: Lightweight Modeling of Structure, Behaviour, and Variability. Art Sci. Eng. Program. 3, 1 (2019), 2. https://doi.org/10.22152/programming-journal.org/2019/3/2
K. Kang, S. Cohen, J. Hess, W. Novak, and S. Peterson. 1990. Feature-Oriented Domain Analysis (FODA) Feasibility Study. Technical Report CMU/SEI-90-TR-21. Carnegie Mellon University.
Jacob Krüger, Sebastian Nielebock, Sebastian Krieter, Christian Diedrich, Thomas Leich, Gunter Saake, Sebastian Zug, and Frank Ortmeier. 2017. Beyond Software Product Lines: Variability Modeling in Cyber-Physical Systems. In SPLC 2017, Proceedings, Myra B. Cohen, Mathieu Acher, Lidia Fuentes, Daniel Schall, Jan Bosch, Rafael Capilla, Ebrahim Bagheri, Yingfei Xiong, Javier Troya, Antonio Ruiz Cortés, and David Benavides (Eds.). ACM, 237-241.
Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV 2011, Proceedings (LNCS, Vol. 6806), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, 585-591.
Kim Guldstrand Larsen, Axel Legay, and Danny Bogsted Poulsen. 2023. Refinement of Systems with an Attacker Focus. In Formal Methods for Industrial Critical Systems-28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 14290), Alessandro Cimatti and Laura Titolo (Eds.). Springer, 96-112. https://doi.org/10.1007/978-3-031-43681-9-6
Sami Lazreg, Maxime Cordy, and Axel Legay. 2022. Verification of variabilityintensive stochastic systems with statistical model checking. In ISoLA 2022, Proceedings. Springer, 448-471.
Amir Pnueli. 1977. The Temporal Logic of Programs. In Annual Symposium on Foundations of Computer Science, 1977. IEEE Computer Society, 46-57.
Klaus Pohl and Andreas Metzger. 2018. Software Product Lines. In The Essence of Software Engineering, Volker Gruhn and Rüdiger Striemer (Eds.). Springer, 185-201. https://doi.org/10.1007/978-3-319-73897-0-11
Maurice H. ter Beek, Ferruccio Damiani, Stefania Gnesi, Franco Mazzanti, and Luca Paolini. 2015. From Featured Transition Systems to Modal Transition Systems with Variability Constraints. In SEFM 2015, Proceedings (LNCS, Vol. 9276), Radu Calinescu and Bernhard Rumpe (Eds.). Springer, 344-359.
Maurice H. ter Beek, Erik P. de Vink, and Tim A. C. Willemse. 2017. Family-Based Model Checking with mCRL2. In FASE 2017, Proceedings (LNCS, Vol. 10202), Marieke Huisman and Julia Rubin (Eds.). Springer, 387-405.
Maurice H. ter Beek, Axel Legay, Alberto Lluch-Lafuente, and Andrea Vandin. 2016. Statistical Model Checking for Product Lines. In ISoLA 2016, Proceedings (LNCS, Vol. 9952), Tiziana Margaria and Bernhard Steffen (Eds.). 114-133.
Maurice H. ter Beek, Axel Legay, Alberto Lluch-Lafuente, and Andrea Vandin. 2021. Quantitative Security Risk Modeling and Analysis with RisQFLan. Comput. Secur. 109 (2021), 102381.
