Towards Strengthening Formal Specifications with Mutation Model Checking

CORDY, Maxime; LAZREG, Sami; Legay, Axel; Schobbens, Pierre Yves

doi:10.1145/3611643.3613080

Download

Paper published in a book (Scientific congresses, symposiums and conference proceedings)

Towards Strengthening Formal Specifications with Mutation Model Checking

CORDY, Maxime; LAZREG, Sami; Legay, Axel et al.

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

Peer reviewed

Permalink
https://hdl.handle.net/10993/59630

DOI
10.1145/3611643.3613080

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

NIER_FSE23-1.pdf

Author postprint (531.32 kB)

Creative Commons License - Attribution, Non-Commercial

Download

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

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

Editor :

Chandra, Satish

Publisher :

Association for Computing Machinery, Inc

ISBN/EAN :

9798400703270

Peer reviewed :

Peer reviewed

Focus Area :

Computational Sciences

Additional URL :

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

FnR Project :

INTER/FNRS/20/15077233/Scaling Up Variability/Cordy

Name of the research project :

Scaling Up Variability

Funders :

FNR Luxembourg INTER/FNRS/20/15077233/Scaling Up Variability/Cordy
FNRS Belgium PDR/PDN - T013721
FNRS Belgium PDR/PDN - T019921F

Funding text :

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).

Available on ORBilu :

since 11 January 2024

Statistics

Number of views

18 (3 by Unilu)

Number of downloads

19 (6 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenAlex citations

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.