Static detection of equivalent mutants in real-time model-based mutation testing: An Empirical Evaluation

mutation-based testing; real-time system; Software product line; Empirical evaluations; Equivalent Mutants; Model-based OPC; Mutation testing; Mutation-based testing; Real - Time system; Real time modeling; Software Product Line; Static detections; Test case; Software

Abstract :

[en] Model-based mutation testing has the potential to effectively drive test generation to reveal faults in software systems. However, it faces a typical efficiency issue since it could produce many mutants that are equivalent to the original system model, making it impossible to generate test cases from them. We consider this problem when model-based mutation testing is applied to real-time system product lines, represented as timed automata. We define novel, time-specific mutation operators and formulate the equivalent mutant problem in the frame of timed refinement relations. Further, we study in which cases a mutation yields an equivalent mutant. Our theoretical results provide guidance to system engineers, allowing them to eliminate mutations from which no test case can be produced. Our empirical evaluation, based on a proof-of-concept implementation and a set of benchmarks from the literature, confirms the validity of our theory and demonstrates that in general our approach can avoid the generation of a significant amount of the equivalent mutants.

Disciplines :

Computer science

Author, co-author :

Basile, Davide ; ISTI–CNR, Pisa, Italy

ter Beek, Maurice H.; ISTI–CNR, Pisa, Italy

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, Ottignies-Louvain-la-Neuve, Belgium

External co-authors :

yes

Language :

English

Title :

Static detection of equivalent mutants in real-time model-based mutation testing: An Empirical Evaluation

Publication date :

December 2022

Journal title :

Empirical Software Engineering

ISSN :

1382-3256

eISSN :

1573-7616

Publisher :

Springer

Volume :

Issue :

Peer reviewed :

Peer Reviewed verified by ORBi

Additional URL :

https://link.springer.com/content/pdf/10.1007/s10664-022-10149-y.pdf

Funding text :

We thank the anonymous reviewers for useful comments and suggestions that helped us to improve the presentation. Davide Basile and Maurice H. ter Beek acknowledge funding from the national MIUR-PRIN 2020TL3X8X project T-LADIES (Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems). Maxime Cordy and Sami Lazreg are supported by FNR Luxembourg (grant INTER/FNRS/20/15077233/Scaling Up Variability/Cordy).

Available on ORBilu :

since 15 December 2023

Statistics

Number of views

72 (3 by Unilu)

Number of downloads

14 (1 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

WoS citations^™

Bibliography

Aichernig BK, Brandl H, Jöbstl E, Krenn W, Schlick R, Tiran S (2015) Killing strategies for model-based mutation testing. Softw Test Verif Reliab 25(8):716–748. 10.1002/stvr.1522 DOI: 10.1002/stvr.1522
Aichernig BK, Lorber F, Nickovic D (2013) Time for mutants: Model-based mutation testing with timed automata. In: Veanes M, Viganò L (eds) Proceedings of the 7th international conference on tests and proofs (TAP’13), LNCS. https://doi.org/10.1007/978-3-642-38916-0_2, vol 7942. Springer, pp 20–38
Alur R, Dill DL (1994) A theory of timed automata. Theoret Comput Sci 126(2):183–235. 10.1016/0304-3975(94)90010-810.1016/0304-3975(94)90010-8 DOI: 10.1016/0304-3975(94)90010-8
André É, Hasuo I, Waga M (2018) Offline timed pattern matching under uncertainty. In: Proceedings of the 23rd international conference on engineering of complex computer systems (ICECCS’18). IEEE, pp 10–20. https://doi.org/10.1109/ICECCS2018.2018.00010
André É, Knapik M, Lime D, Penczek W, Petrucci L (2019) Parametric verification: an introduction. In: Koutny M, Pomello L, Kristensen LM (eds) Transactions on petri nets and other models of concurrency XIV, LNCS. https://doi.org/10.1007/978-3-662-60651-3_3, vol 11790. Springer, pp 64–100
Andrews JH, Briand LC, Labiche Y, Namin AS (2006) Using mutation analysis for assessing and comparing testing coverage criteria. IEEE Trans Softw Eng 32(8):608–624. 10.1109/TSE.2006.83 DOI: 10.1109/TSE.2006.83
Asarin E, Maler O, Pnueli A, Sifakis J (1998) Controller synthesis for timed automata. IFAC Proc 31(18):447–452. 10.1016/S1474-6670(17)42032-5. Proceedings of the 5th IFAC conference on system structure and control (SSC’98) DOI: 10.1016/S1474-6670(17)42032-5
Baker R, Habli I (2013) An empirical evaluation of mutation testing for improving the test quality of safety-critical software. IEEE Trans Softw Eng 39 (6):787–805. 10.1109/TSE.2012.56 DOI: 10.1109/TSE.2012.56
Basile D, ter Beek MH, Cordy M, Legay A (2020a) Tackling the equivalent mutant problem in real-time systems: The 12 commandments of model-based mutation testing. In: Proceedings of the 24th ACM conference on systems and software product lines (SPLC’20). ACM, pp 252–262. https://doi.org/10.1145/3382025.3414966 https://doi.org/10.1145/3382025.3414966
Basile D, ter Beek MH, Degano P, Legay A, Ferrari GL, Gnesi S, Di Giandomenico F (2020b) Controller synthesis of service contracts with variability. Sci Comput Program, 187. 10.1016/j.scico.2019.10234410.1016/j.scico.2019.102344
Basile D, ter Beek MH, Legay A (2020c) Timed service contract automata. Innovations Syst Softw Eng (16), 199–214. 10.1007/s11334-019-00353-3
Behrmann G, Cougnard A, David A, Fleury E, Larsen KG, Lime D (2007) UPPAAL-Tiga: time for playing games! In: Damm W, Hermanns H (eds) Proceedings of the 19th international conference on computer aided verification (CAV’07), LNCS, vol 4590. Springer, pp 121–125. https://doi.org/10.1007/978-3-540-73368-3_14
Benes N, Bezdek P, Larsen KG, Srba J (2015) Language emptiness of continuous-time parametric timed automata. In: Halldórsson MM, Iwama K, Kobayashi N, Speckmann B (eds) Proceedings of the 42nd international colloquium on automata, languages, and programming (ICALP’15), LNCS. https://doi.org/10.1007/978-3-662-47666-6_6, vol 9135. Springer, pp 69–81
Brillout A, He N, Mazzucchi M, Kroening D, Purandare M, Rümmer P, Weissenbacher G (2009) Mutation-based test case generation for Simulink models. In: De Boer FS, Bonsangue MM, Hallerstede S, Leuschel M (eds) Proceedings of the 8th international symposium on formal methods for components and objects (FMCO’09), LNCS. https://doi.org/10.1007/978-3-642-17071-3_11, vol 6286. Springer, pp 208–227
Chow TS (1978) Testing software design modeled by finite-state machines. IEEE Trans Softw Eng SE-4(3):178–187. 10.1109/TSE.1978.231496 DOI: 10.1109/TSE.1978.231496
Classen A, Cordy M, Schobbens P, Heymans P, Legay A, Raskin J (2013) Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans Softw Eng 39 (8):1069–1089. 10.1109/TSE.2012.86 DOI: 10.1109/TSE.2012.86
Cordy M, Classen A, Perrouin G, Schobbens P, Heymans P, Legay A (2012a) Simulation-based abstractions for software product-line model checking. In: Proceedings of the 34th international conference on software engineering (ICSE’12). IEEE, pp 672–682. https://doi.org/10.1109/ICSE.2012.6227150
Cordy M, Schobbens P, Heymans P, Legay A (2012b) Behavioural modelling and verification of real-time software product lines. In: Proceedings of the 16th international software product line conference (SPLC’12). ACM, pp 66–75. https://doi.org/10.1145/2362536.2362549
Cordy M, Legay A, Schobbens P, Traonouez L (2013) A framework for the rigorous design of highly adaptive timed systems. In: Proceedings of the 1st FME workshop on formal methods in software engineering (FormaliSE’13). IEEE, pp 64–70. https://doi.org/10.1109/FormaliSE.2013.6612279
David A, Larsen KG, Legay A, Nyman U, Traonouez L, Wa̧sowski A (2015) Real-time specifications. Int J Softw Tools Technol Transf 17 (1):17–45. 10.1007/s10009-013-0286-x DOI: 10.1007/s10009-013-0286-x
David A, Larsen KG, Legay A, Nyman U, Wa̧sowski A. (2010a) Timed I/O automata: a complete specification theory for real-time systems. In: Proceedings of the 13th international conference on hybrid systems: computation and control (HSCC’10). ACM, pp 91–100. https://doi.org/10.1145/1755952.1755967
David A, Larsen KG, Legay A, Nyman U, Wa̧sowski A (2010b) ECDAR: an environment for compositional design and analysis of real time systems. In: Bouajjani A, Chin WN (eds) Proceedings of the 8th international symposium on automated technology for verification and analysis (ATVA’10), LNCS. https://doi.org/10.1007/978-3-642-15643-4_29, vol 6252. Springer, pp 365–370
DeMillo R, Lipton R, Sayward F (1978) Hints on test data selection: Help for the practicing programmer. IEEE Comp 11(4):34–41. 10.1109/C-M.1978.218136 DOI: 10.1109/C-M.1978.218136
Devroey X, Perrouin G, Papadakis M, Legay A, Schobbens P, Heymans P (2016) Featured model-based mutation analysis. In: Proceedings of the 38th international conference on software engineering (ICSE’16). ACM, pp 655–666. https://doi.org/10.1145/2884781.2884821
Fabbri S, Maldonado JC, Sugeta T, Masiero PC (1999) Mutation testing applied to validate specifications based on statecharts. In: Proceedings of the 10th international symposium on software reliability engineering (ISSRE’99). IEEE, pp 210–219. https://doi.org/10.1109/ISSRE.1999.809326
Feo-Arenis S, Westphal B, Dietsch D, Muñiz M, Andisha AS (2014) The wireless fire alarm system: ensuring conformance to industrial standards through formal verification. In: Jones C, Pihlajasaari P, Sun J (eds) Proceedings of the 19th international symposium on formal methods (FM’14), LNCS. 10.1007/978-3-319-06410-9_44, vol 8442. Springer, pp 658–672
Hoxha B, Abbas H, Fainekos G (2015) Benchmarks for temporal logic requirements for automotive systems. In: Frehse G, Althoff M (eds) Proceedings of the 1st and 2nd international workshop on applied verification for continuous and hybrid systems (ARCH’14-’15), EPiC Series in Computing. 10.29007/xwrs, vol 34. EasyChair, pp 25–30
Hune T, Romijn J, Stoelinga M, Vaandrager FW (2001) Linear parametric model checking of timed automata. Tech. Rep. CSI-R0102, University of Nijmegen. http://hdl.handle.net/2066/18941
Jia Y, Harman M (2011) An analysis and survey of the development of mutation testing. IEEE Trans Softw Eng 37(5):649–678. 10.1109/TSE.2010.62 DOI: 10.1109/TSE.2010.62
Lamport L (1987) A fast mutual exclusion algorithm. ACM Trans Comput Syst 5(1):1–11. 10.1145/7351.7352 DOI: 10.1145/7351.7352
Larsen KG, Lorber F, Nielsen B, Nyman U (2017) Mutation-based test-case generation with Ecdar. In: Proceedings of the 10th IEEE international conference on software testing, verification and validation workshops (ICSTW’17). IEEE, pp 319–328. https://doi.org/10.1109/ICSTW.2017.60
Larsen KG, Nyman U, Wa̧sowski A (2007) Modal I/O automata for interface and product line theories. In: De Nicola R (ed) Proceedings of the 16th european symposium on programming (ESOP’07), LNCS. https://doi.org/10.1007/978-3-540-71316-6_6, vol 4421. Springer, pp 64–79
Lee J, Kang S, Jung P (2020) Test coverage criteria for software product line testing: Systematic literature review. Inf Softw Technol, 122. 10.1016/j.infsof.2020.106272
Luthmann L, Gerecht T, Lochau M (2019) Sampling strategies for product lines with unbounded parametric real-time constraints. Int J Softw Tools Technol Transf 21(6):613–633. 10.1007/s10009-019-00532-4 DOI: 10.1007/s10009-019-00532-4
Luthmann L, Stephan A, Bürdek J, Lochau M (2017) Modeling and testing product lines with unbounded parametric real-time constraints. In: Proceedings of the 21st international systems and software product lines conference (SPLC’17). ACM, pp 104–113. https://doi.org/10.1145/3106195.3106204
Madeyski L, Orzeszyna W, Torkar R, Józala M (2014) Overcoming the equivalent mutant problem: a systematic literature review and a comparative experiment of second order mutation. IEEE Trans Softw Eng 40(1):23–42. 10.1109/TSE.2013.44 DOI: 10.1109/TSE.2013.44
Masri W, Zaraket F (2016) Coverage-based software testing: Beyond basic test requirements. In: Memon AM (ed) Advances in computers, vol 103, chap 4. Elsevier, pp 79–142. https://doi.org/10.1016/bs.adcom.2016.04.003
Offutt J (2011) A mutation carol: past, present and future. Inf Softw Technol 53(10):1098–1107. 10.1016/j.infsof.2011.03.007 DOI: 10.1016/j.infsof.2011.03.007
Papadakis M, Malevris N (2010) An empirical evaluation of the first and second order mutation testing strategies. In: Proceedings of the 3rd international conference on software testing, verification and validation workshops (ICSTW’10), pp 90–99. https://doi.org/10.1109/ICSTW.2010.50
Petrovic G, Ivankovic M, Fraser G, Just R (2021) Does mutation testing improve testing practices?. In: 43rd IEEE/ACM international conference on software engineering (ICSE’21). IEEE, pp 910–921. 10.1109/ICSE43902.2021.00087
Ter Beek, Cledou G, Hennicker R, Proença J (2021) Featured team automata. In: Huisman M, Pasareanu CS, Zhan N (eds) Proceedings of the 24th international symposium on formal methods (FM’21), LNCS, vol 13047. Springer, pp 483–502. 10.1007/978-3-030-90870-6_26
Ter Beek MH, Kleijn J (2012) Vector team automata. Theor Comput Sci 429:21–29. 10.1016/j.tcs.2011.12.020 DOI: 10.1016/j.tcs.2011.12.020
Ter Beek MH, van Loo S, De Vink EP, Willemse TA (2020) Family-based SPL model checking using parity games with variability. In: Wehrheim H, Cabot J (eds) Proceedings of the 23rd international conference on fundamental approaches to software engineering (FASE’20), LNCS. https://doi.org/10.1007/978-3-030-45234-6_12, vol 12076. Springer, pp 245–265
Ter Beek MH, Fantechi A, Gnesi S, Mazzanti F (2016) Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints. J Log Algebr Meth Program 85(2):287–315. 10.1016/j.jlamp.2015.11.006 DOI: 10.1016/j.jlamp.2015.11.006
Utting M, Pretschner A, Legeard B (2012) A taxonomy of model-based testing approaches. Softw Test Verif Reliab 22(5):297–312. 10.1002/stvr.456 DOI: 10.1002/stvr.456
Waga M, Hasuo I, Suenaga K (2017) Efficient online timed pattern matching by automata-based skipping. In: Abate A, Geeraerts G (eds) Proceedings of the 15th international conference on formal modeling and analysis of timed systems (FORMATS’17), LNCS. https://doi.org/10.1007/978-3-319-65765-3_13, vol 10419. Springer, pp 224–243
Weyuker E, Goradia T, Singh A (1994) Automatically generating test data from a Boolean specification. IEEE Trans Softw Eng 20(5):353–363. 10.1109/32.286420 DOI: 10.1109/32.286420