model-based testing; mutation testing; timed automata; UPPAAL; % reductions; Bisimulations; Model based testing; Model-based systems; Mutation testing; Real time modeling; Safety critical systems; Test quality; Timed Automata; Software; Safety, Risk, Reliability and Quality
Abstract :
[en] To assess test quality, mutation testing (MT) creates mutants by injecting artificial faults into the system and evaluates the ability of tests to distinguish these mutants. Tests distinguishing more mutants have also been proven empirically to detect more real faults. MT has been applied to many domains. We focus on MT for timed safety-critical systems modelled as Timed Automata (TA). While powerful, MT usually yields equivalent and duplicate mutants, the former having the same behaviour as the original system and the latter other mutants. Such useless mutants bring no value, waste execution time and can be difficult to detect. We integrate useless mutant detection and removal strategies in our mutation framework MUPPAAL. MUPPAAL leverages existing equivalence-avoiding mutation operators and focuses on detecting mutant duplicates using a scalable bisimulation algorithm and a fast approximate one based on biased simulation. We also demonstrate how to design an operator that reduces the occurrence of mutant duplicates. We evaluate MUPPAAL on six systems, demonstrating that (1) mutant duplicates account for up to 32% of all generated mutants, (2) our bisimulation approach scales effectively with these systems and (3) biased simulations further enhance performance. Our heuristic is 10 times faster than bisimulation and limits the exploration to two times the number of exact duplicates compared to up to 10 times for the baseline.
Disciplines :
Computer science
Author, co-author :
Cuartas, Jaime; Faculty of Information Technology, Monash University, Melbourne, Australia
Cortés, David ; EISC, Universidad del Valle, Cali, Colombia
Betancourt, Joan; EISC, Universidad del Valle, Cali, Colombia
Aranda, Jesús; EISC, Universidad del Valle, Cali, Colombia
CORDY, Maxime ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SerVal
Ortiz, James ; LTCI, Télécom Paris, Institut Polytechnique de Paris, Palaiseau, France
Perrouin, Gilles ; Faculty of Computer Science, University of Namur, Namur, Belgium
Schobbens, Pierre-Yves ; Faculty of Computer Science, University of Namur, Namur, Belgium
External co-authors :
yes
Language :
English
Title :
MUPPAAL: Efficient Elimination and Reduction of Useless Mutants in Real-Time Model-Based Systems
Gilles Perrouin is an Fnrs (Fonds National de la Recherche Scientifique) Research Associate. Jaime Cuartas received support from ERASMUS+ while at the University of Namur. Maxime Cordy obtained funding from FNR Luxembourg (grant INTER/FNRS/20/15077233/Scaling Up Variability/Cordy). Work partially funded by ERDF project IDEES. Thanks to the multilateral agreement between the University of Namur and Universidad del Valle.
J. Tretmans, Formal Methods and Testing—An Outcome of the FORTEST Network (Revised Papers Selection) (Springer-Verlag, 2008): 1–38, http://dl.acm.org/citation.cfm?id=1806209.1806210.
J. Zander, I. Schieferdecker, and P. J. Mosterman, Model-Based Testing for Embedded Systems (CRC Press, 2017).
Y. Jia and M. Harman, “An Analysis and Survey of the Development of Mutation Testing,” IEEE Transactions on Software Engineering 37, no. 5 (2011): 649–678, https://doi.org/10.1109/TSE.2010.62.
M. Papadakis, Y. Jia, M. Harman, and Y. Le Traon, “Trivial Compiler Equivalence: A Large Scale Empirical Study of a Simple Fast and Effective Equivalent Mutant Detection Technique,” in International Conference on Software Engineering, ICSE (IEEE, 2015): 936–946.
M. Papadakis and N. Malevris, “Automatic Mutation Test Case Generation via Dynamic Symbolic Execution,” in ISSRE (IEEE, 2010): 121–130.
G. Fraser and A. Arcuri, “Achieving Scalable Mutation-Based Generation of Whole Test Suites,” Empirical Software Engineering 20 (2014): 783–812.
J. Offutt, “A Mutation Carol: Past, Present and Future,” Information and Software Technology 53, no. 10 (2011): 1098–1107.
T. A. Budd and A. S. Gopal, “Program Testing by Specification Mutation,” Computer Languages 10, no. 1 (1985): 63–73.
W. E. Howden, “Reliability of the Path Analysis Testing Strategy,” IEEE Transactions on Software Engineering 2, no. 3 (1976): 208–215.
J. M. Voas and G. McGraw, Software Fault Injection: Inoculating Programs Against Errors (New York, NY, USA: John Wiley & Sons, Inc., 1997).
M. Papadakis, M. Kintis, J. Zhang, Y. Jia, Y. L. Traon, and M. Harman, “Mutation Testing Advances: An Analysis and Survey,” Advances in Computers 2019 (2019): 275–378.
D. Basile, M. H. Beek, S. Lazreg, M. Cordy, and A. Legay, “Static Detection of Equivalent Mutants in Real-Time Model-Based Mutation Testing,” Empirical Software Engineering 27, no. 7 (2022): 160, https://doi.org/10.1007/s10664-022-10149-y.
D. Basile, M. H. Ter Beek, M. Cordy, and A. Legay, “Tackling the Equivalent Mutant Problem in Real-Time Systems: The 12 Commandments of Model-Based Mutation Testing,” in SPLC '20: 24th ACM International Systems and Software Product Line Conference, Montreal, Quebec, Canada, October 19–23, 2020, Volume A Edited by R. E. Lopez-Herrejon, (ACM, 2020): 30:1–30:11, https://doi.org/10.1145/3382025.3414966.
G. Behrmann, A. David, and K. G. Larsen, “A Tutorial on uppaal,” in Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004 Edited by M. Bernardo and F. Corradini, LNCS, (Springer–Verlag, 2004): 200–236.
J. Betancourt, J. Ortiz, and J. Aranda, “Applying Parallelism to a Bisimulation Algorithm to Improve Efficiency in Software Testing of Time-Critical Systems,” Ingeniería y Competitividad 25, no. Suplemento (2023): e–20713144, https://revistaingenieria.univalle.edu.co/index.php/ingenieria_y_competitividad/article/view/13144.
J. J. Ortiz, M. Amrani, and P.-Y. Schobbens, “Multi-Timed Bisimulation for Distributed Timed Automata,” in NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings Edited by C. Barrett, M. Davies, and T. Kahsai, Lecture Notes in Computer Science, Vol. 10227, (2017): 52–67, https://doi.org/10.1007/978-3-319-57288-8.
X. Devroey, G. Perrouin, M. Papadakis, A. Legay, P.-Y. Schobbens, and P. Heymans, “Model-Based Mutant Equivalence Detection Using Automata Language Equivalence and Simulations,” Journal of Systems and Software 141 (2018): 1–15, https://www.sciencedirect.com/science/article/pii/S0164121218300475.
K. G. Larsen, M. Mikucionis, and B. Nielsen, “Testing Real-Time Embedded Software Using UPPAAL-TRON: An Industrial Case Study,” in The 5th ACM International Conference on Embedded Software (ACM Press New York, NY, USA, 2005): 299–306, http://doi.acm.org/10.1145/1086228.1086283.
B. K. Aichernig, J. Auer, E. Jöbstl, et al., “Model-Based Mutation Testing of an Industrial Measurement Device,” in Tests and Proofs, LNCS, Vol. 8570, (Springer, 2014): 1–19.
J. Cuartas, J. Aranda, M. Cordy, J. Ortiz, G. Perrouin, and P.-Y. Schobbens, “Muppaal: Reducing and Removing Equivalent and Duplicate Mutants in UPPAAL,” in 2023 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), (2023): 52–61.
R. Alur and D. L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science 126, no. 2 (1994): 183–235, https://doi.org/10.1016/0304-3975(94)90010-8.
M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine, “Kronos: A Model-Checking Tool for Real-Time Systems,” in Computer Aided Verification 10th International Conference, CAV'98 Edited by A. J. Vardi and Y. M. Hu, Lecture Notes in Computer Science, Vol. 1427, (Vancouver, BC, Canada, 1998): 546–549, https://hal.archives-ouvertes.fr/hal-00374784.
T. A. Henzinger, P.-H. Ho, and H. Wong-toi, “Hytech: A Model Checker for Hybrid Systems,” Software Tools for Technology Transfer 1 (1997): 460–463.
B. K. Aichernig, F. Lorber, and D. Nickovic, “Time for Mutants—Model-Based Mutation Testing With Timed Automata,” in Proceedings Tests and Proofs - 7th International Conference, TAP 2013, Budapest, Hungary, June 16-20, 2013 Edited by M. Veanes and L. Viganò, Lecture Notes in Computer Science, Vol. 7942, (Springer, 2013): 20–38.
A. David, K. G. Larsen, A. Legay, U. Nyman, and A. Wasowski, “Timed I/O Automata: A Complete Specification Theory for Real-Time Systems,” in Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC '10, (New York, NY, USA: ACM, 2010): 91–100, http://doi.acm.org/10.1145/1755952.1755967.
D. K. Kaynar, N. A. Lynch, R. Segala, and F. W. Vaandrager, The Theory of Timed I/O Automata, Second Edition, Synthesis Lectures on Distributed Computing Theory, (Morgan & Claypool Publishers, 2010), https://doi.org/10.2200/S00310ED1V01Y201011DCT005.
K. Cerāns, “Decidability of Bisimulation Equivalences for Parallel Timer Processes,” in Proceedings of the 4th International Workshop on Computer Aided Verification (CAV'92) Edited by G. von Bochmann and D. K. Probst, Lecture Notes in Computer Science, Vol. 663, (Springer-Verlag, 1993): 302–315.
R. Nilsson, J. Offutt, and S. F. Andler, “Mutation-Based Testing Criteria for Timeliness,” in Proceedings of the 28th Annual International Computer Software and Applications Conference, COMPSAC '04, (Washington, DC, USA, 2004): 306–311, http://dl.acm.org/citation.cfm?id=1025117.1025515.
R. M. Hierons, S. Counsell, and M. AbouTrab, “Specification Mutation Analysis for Validating Timed Testing Approaches Based on Timed Automata,” in 2013 IEEE 37th Annual Computer Software and Applications Conference, (Los Alamitos, CA, USA, 2012): 660–669, https://doi.ieeecomputersociety.org/10.1109/COMPSAC.2012.93.
K. G. Larsen, F. Lorber, B. Nielsen, and U. M. Nyman, “Mutation-Based Test-Case Generation With ECDAR,” in 2017 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), (2017): 319–328.
R. Just, D. Jalali, L. Inozemtseva, M. D. Ernst, R. Holmes, and G. Fraser, “Are Mutants a Valid Substitute for Real Faults in Software Testing?,”in Fse 2014: Proceedings of the ACM SIGSOFT 22nd Symposium on the Foundations of Software Engineering, (Hong Kong, 2014): 654–665.
R. M. Hierons, J. P. Bowen, and M. Harman Eds., Formal Methods and Testing, an Outcome of the FORTEST Network, Revised Selected Papers Edited by R. M. Hierons, J. P. Bowen, and M. Harman, Lecture Notes in Computer Science, Vol. 4949, (Springer, 2008), https://doi.org/10.1007/978-3-540-78917-8.
L. Madeyski, W. Orzeszyna, R. Torkar, and M. Józala, “Overcoming the Equivalent Mutant Problem: A Systematic Literature Review and a Comparative Experiment of Second Order Mutation,” IEEE Transactions on Software Engineering 40, no. 1 (2014): 23–42.
K. Adamopoulos, M. Harman, and R. M. Hierons, “How to Overcome the Equivalent Mutant Problem and Achieve Tailored Selective Mutation Using Co-Evolution,” in Proceedings, Part II Genetic and Evolutionary Computation–GECCO 2004: Genetic and Evolutionary Computation Conference, Seattle, WA, USA, June 26–30, 2004. Springer, (2004): 1338–1349.
A. J. Offutt and J. Pan, “Automatically Detecting Equivalent Mutants and Infeasible Paths,” Software testing, Verification and Reliability 7, no. 3 (1997): 165–192.
M. Kintis, M. Papadakis, Y. Jia, N. Malevris, Y. Le Traon, and M. Harman, “Detecting Trivial Mutant Equivalences via Compiler Optimisations,” IEEE Transactions on Software Engineering 44, no. 4 (2018): 308–333.
B. Kushigian, S. Kaufman, R. Featherman, H. Potter, A. Madadi, and R. Just, “Equivalent Mutants in the Wild: Identifying and Efficiently Suppressing Equivalent Mutants for Java Programs,” in Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing And analysis (ISSTA '24), (2024).
Z. Tian, H. Shu, D. Wang, X. Cao, Y. Kamei, and J. Chen, “Large Language Models for Equivalent Mutant Detection: How Far Are We?,”in Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '24), (2024), https://arxiv.org/abs/2408.01760.
K. Guldstrand Larsen, M. Mikucionis, and B. Nielsen, “UPPAAL Tron User Manual—docs.uppaal.org,” (2017), https://docs.uppaal.org/extensions/tron/manual.pdf.
T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic Model Checking for Real Time Systems,” Information and Computation 111, no. 2 (1994): 193–244.
B. Kurtz, P. Ammann, J. Offutt, and M. Kurtz, “Are We There Yet? How Redundant and Equivalent Mutants Affect Determination of Test Completeness,” in Ninth IEEE International Conference on Software Testing, Verification and Validation Workshops, ICST Workshops 2016, Chicago, IL, USA, April 11-15, 2016 (IEEE Computer Society, 2016): 142–151, https://doi.org/10.1109/ICSTW.2016.41.
C. Baier and J. P. Katoen, Principles of Model Checking, MIT Press, (MIT Press, 2008).
V. Jayapaul, J. I. Munro, V. Raman, and S. R. Satti, “Sorting and Selection With Equality Comparisons,” in Algorithms and Data Structures Edited by F. Dehne, J.-R. Sack, and U. Stege, (Cham: Springer International Publishing, 2015): 434–445.
T. Parr, The Definitive ANTLR 4 Reference, 2nd ed., (Raleigh, NC: Pragmatic Bookshelf, 2013).
S. Bardin, M. Delahaye, R. David, et al., “Sound and Quasi-Complete Detection of Infeasible Test Requirements,” in 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST) (IEEE, 2015): 1–10.
W. Krenn and R. Schlick, “Mutation-Driven Test Case Generation Using Short-Lived Concurrent Mutants—First Results,” (2016), arXiv preprint arXiv:1601.06974.
M. Lindahl, P. Pettersson, and W. Yi, “Formal Design and Analysis of a Gear Controller,” International Journal on Software Tools for Technology Transfer 3, no. 3 (2001): 353–368, https://doi.org/10.1007/s100090100048.
H. Jensen, K. Larsen, and A. Skou, “Modelling and Analysis of a Collision Avoidance Protocol Using Spin and UPPAAL,” BRICS Report Series 3 (2002): 23–42.
R. Alur, T. A. Henzinger, and M. Y. Vardi, “Parametric Real-Time Reasoning,” in STOC (ACM, 1993): 592–601.
A. David, J. Illum, K. G. Larsen, and A. Skou, “Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1,” in Model-Based Design for Embedded Systems (CRC Press, 2018): 117–144.
L. Luthmann, H. Göttmann, I. Bacher, and M. Lochau, “Checking Timed Bisimulation With Bounded Zone-History Graphs—Technical Report,” (2020).
D. Cortés, J. Ortiz, D. Basile, J. Aranda, G. Perrouin, and P. Y. Schobbens, “Time for Networks: Mutation Testing for Timed Automata Networks,” in Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (Formalise), FormaliSE '24, (New York, NY, USA: Association for Computing Machinery, 2024): 44–54, https://doi.org/10.1145/3644033.3644378.
X. Devroey, G. Perrouin, M. Papadakis, P.-Y. Schobbens, and P. Heymans, “Featured Model-Based Mutation Analysis,” in International Conference on Software Engineering, ICSE, (Austin, TX, USA, 2016).
S. C. P. F. Fabbri, J. C. Maldonado, T. Sugeta, and P. C. Masiero, “Mutation Testing Applied to Validate Specifications Based on Statecharts,” in Proceedings of the 10th International Symposium on Software Reliability Engineering, ISSRE '99, (Washington, DC, USA, 1999): 210, http://dl.acm.org/citation.cfm?id=851020.856195.
J. J. O. Vega, G. Perrouin, M. Amrani, and P.-Y. Schobbens, “Model-Based Mutation Operators for Timed Systems: A Taxonomy and Research Agenda,” in 2018 IEEE International Conference on Software Quality, Reliability and Security (QRS), (2018).
A. David, K. G. Larsen, A. Legay, U. M. Nyman, and A. Wasowski, “ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems,” in Lecture Notes in Computer Science, Vol. 6252/2010, (Germany, 2010).
A. Hessel and P. Pettersson, “Cover—A Test-Case Generation Tool for Timed Systems,” Testing of Software and Communicating Systems 1 (2007): 31–34.
T. R. Gundersen, F. Lorber, U. Nyman, and C. Ovesen, “Effortless Fault Localisation: Conformance Testing of Real-Time Systems in ECDAR,” Electronic Proceedings in Theoretical Computer Science 277 (2018): 147–160, https://doi.org/10.4204/EPTCS.277.11.
J. H. Kim, K. G. Larsen, B. Nielsen, M. Mikucionis, and P. Olsen, “Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools,” in Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings Edited by M. Núñez and M. Güdemann, Lecture Notes in Computer Science, Vol. 9128, (Springer, 2015): 47–61, https://doi.org/10.1007/978-3-319-19458-5_4.
F. Siavashi, J. Iqbal, D. Truscan, and J. Vain, “Testing Web Services With Model-Based Mutation,” in Software Technologies (Springer, 2017): 45–67.
