2023 • In Chandra, Satish (Ed.) ESEC/FSE 2023 - Proceedings of the 31st ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering
LTL; Model checking; Models checking; Mutation testing; Artificial Intelligence; Software
Abstract :
[en] We propose mutation model checking as an approach to strengthen formal specifications used for model checking. Inspired by mutation testing, our approach concludes that specifications are not strong enough if they fail to detect faults in purposely mutated models. Our preliminary experiments on two case studies confirm the relevance of the problem: their specification can only detect 40% and 60% of randomly generated mutants. As a result, we propose a framework to strengthen the original specification, such that the original model satisfies the strengthened specification but the mutants do not.
Disciplines :
Computer science
Author, co-author :
CORDY, Maxime ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SerVal
LAZREG, Sami ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SerVal
Legay, Axel ; Université Catholique de Louvain, Belgium
Schobbens, Pierre Yves ; University of Namur, Belgium
External co-authors :
yes
Language :
English
Title :
Towards Strengthening Formal Specifications with Mutation Model Checking
Publication date :
30 November 2023
Event name :
Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering
Event place :
San Francisco, Usa
Event date :
03-12-2023 => 09-12-2023
Audience :
International
Main work title :
ESEC/FSE 2023 - Proceedings of the 31st ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering
Maxime Cordy and Sami Lazreg are supported by FNR Luxembourg (INTER/FNRS/20/15077233/Scaling Up Variability/Cordy). Axel Legay and Pierre-Yves are supported by FNRS Belgium (respectively, grants PDR/PDN - T013721 and T019921F).
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.
Bibliography
Bernhard K Aichernig. 2003. Mutation testing in the re_nement calculus. Formal Aspects of Computing 15, 2 (2003), 280-295.
Bernhard K Aichernig. 2013. Model-based mutation testing of reactive systems. In Theories of Programming and Formal Methods. Springer, 23-36.
Paul E Ammann, Paul E Black, and William Majurski. 1998. Using model checking to generate tests from specifications. In Proceedings second international conference on formal engineering methods (Cat. No. 98EX241). IEEE, 46-54.
Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press.
Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press.
Timothy A Budd and Ajei S Gopal. 1985. Program testing by specification mutation. Computer languages 10, 1 (1985), 63-73.
Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, and Bow-Yaw Wang. 2009. Learning Minimal Separating DFA's for Compositional Verification. In Tools and Algorithms for the Construction and Analysis of Systems, 15th Interna-tional Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceed-ings (Lecture Notes in Computer Science, Vol. 5505), Stefan Kowalewski and Anna Philippou (Eds.). Springer, 31-45. https: //doi. org/10. 1007/978-3-642-00768-2_3
Yu-Fang Chen and Bow-Yaw Wang. 2013. BULL: A Library for Learning Algorithms of Boolean Functions. In Tools and Algorithms for the Construction and Analysis of Systems-19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Computer Sci-ence, Vol. 7795), Nir Piterman and Scott A. Smolka (Eds.). Springer, 537-542. https: //doi. org/10. 1007/978-3-642-36742-7_38
Edmund M Clarke, Orna Grumberg, and David E Long. 1994. Model checking and abstraction. ACM transactions on Programming Languages and Systems (TOPLAS) 16, 5 (1994), 1512-1542.
Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). 2018. Handbook of Model Checking. Springer. https: //doi. org/10. 1007/978-3-319-10575-8
Andreas Classen. 2010. Modelling with FTS: A collection of illustrative examples. PReCISE Research Center, University of Namur, Namur, Belgium, Tech. Rep. P-CS-TR SPLMC-00000001 (2010).
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. Transactions on Software Engineering (2013), 1069-1089.
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 Comput. 33, 6 (2021), 1147-1172. https: //doi. org/10. 1007/s00165-021-00563-2
Uli Fahrenberg, Axel Legay, and Louis-Marie Traonouez. 2014. Specification Theories for Probabilistic and Real-Time Systems. In From Programs to Systems. The Systems perspective in Computing-ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8415), Saddek Bensalem, Yassine Lakhnech, and Axel Legay (Eds.). Springer, 98-117. https: //doi. org/10. 1007/978-3-642-54848-2_7
Mark Gabel and Zhendong Su. 2008. Symbolic mining of temporal specifications. In Proceedings of the 30th international conference on Software engineering. 51-60.
Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel. 2020. Manthan: A Data-Driven Approach for Boolean Function Synthesis. In Computer Aided Verification-32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 12225), Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 611-633. https: //doi. org/10. 1007/978-3-030-53291-8_31
G. J. Holzmann. 2004. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley.
Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. 2022. Correction to: Reactive synthesis without regret. Acta Informatica 59, 5 (2022), 671. https: //doi. org/10. 1007/s00236-021-00410-0
J. Kramer, J. Magee, M. Sloman, and A. Lister. 1983. CONIC: An integrated approach to distributed computer control systems. Computers and Digital Tech-niques, IEE Proceedings E 130, 1 (1983), 1-10.
Willibald Krenn and Bernhard K Aichernig. 2009. Test case generation by contract mutation in spec. Electronic Notes in Theoretical Computer Science 253, 2 (2009), 71-86.
J Lång et al. 2017. ADAPOS: An Architecture for Publishing ALICE DCS Conditions Data. In Proc. of International Conference on Accelerator and Large Experi-mental Physics Control Systems (ICALEPCS'17), Barcelona, Spain. 8-13.
John Lång and ISWB Prasetya. 2019. Model checking a C++ software framework: A case study. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 1026-1036.
Louis Latour. 2004. From Automata to Formulas: Convex Integer Polyhedra. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. IEEE Computer Society, 120-129. https: //doi. org/10. 1109/LICS. 2004. 1319606
Axel Legay, Anna Lukina, Louis-Marie Traonouez, Junxing Yang, Scott A. Smolka, and Radu Grosu. 2019. Statistical Model Checking. In Computing and Software Science-State of the Art and Perspectives, Bernhard Steflen and Gerhard J. Woeginger (Eds.). Lecture Notes in Computer Science, Vol. 10000. Springer, 478-504. https: //doi. org/10. 1007/978-3-319-91908-9_23
Caroline Lemieux, Dennis Park, and Ivan Beschastnikh. 2015. General LTL specification mining (T). In 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 81-92.
Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu. 2021. A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. Inf. Comput. 281 (2021), 104678. https: //doi. org/10. 1016/j. ic. 2020. 104678
Daniel Neider and Ivan Gavran. 2018. Learning linear temporal properties. In 2018 Formal Methods in Computer Aided Design (FMCAD). IEEE, 1-10.
Mike Papadakis, Marinos Kintis, Jie Zhang, Yue Jia, Yves Le Traon, and Mark Harman. 2019. Mutation testing advances: An analysis and survey. In Advances in Computers. Vol. 112. Elsevier, 275-378.
Malte Plath and Mark Ryan. 2001. Feature integration using a feature construct. SCP 41, 1 (2001), 53-84.
Thitima Srivatanakul, John A Clark, Susan Stepney, and Fiona Polack. 2003. Challenging formal specifications by mutation: A CSP security example. In Tenth Asia-Pacific Software Engineering Conference, 2003. IEEE, 340-350.
Chang-Ai Sun, Feifei Xue, Huai Liu, and Xiangyu Zhang. 2017. A path-aware approach to mutant reduction in mutation testing. Inf. Softw. Technol. 81 (2017), 65-81. https: //doi. org/10. 1016/j. infsof. 2016. 02. 006
Moshe Y. Vardi and Pierre Wolper. 1986. An automata-theoretic approach to automatic program verification. In LICS'86. IEEE CS, 332-344.
Guido Wimmel and Jan Jürjens. 2002. Specification-based test generation for security-critical systems using mutations. In International Conference on Formal Engineering Methods. Springer, 471-482.
