Model-Based Testing; Mutation Testing; Timed Automata; UPPAAL; Assessment technique; Bisimulations; Model based testing; Mutation testing; Original systems; Quality assessment; Test case; Test quality; Software; Safety, Risk, Reliability and Quality; Modeling and Simulation
Abstract :
[en] Mutation Testing (MT) is a test quality assessment technique that creates mutants by injecting artificial faults into the system and evaluating the ability of tests to distinguish these mutants. We focus on MT for safety-critical Timed Automata (TA). MT is prone to equivalent and duplicate mutants, the former having the same behaviour as the original system and the latter other mutants. Such mutants bring no value and induce useless test case executions. We propose MUPPAAL, a tool that: (1) offers a new operator reducing the occurrence of mutant duplicates; (2) an efficient bisimulation algorithm removing remaining duplicates; (3) leverages existing equivalence-avoiding mutation operators. Our experiments on four UPPAAL case studies indicate that duplicates represent up to 32% of all mutants and that the MUPPAAL bisimulation algorithm can identify them more than 99% of the time.
Disciplines :
Computer science
Author, co-author :
Cuartas, Jaime; Universidad Del Valle, Cali, Colombia
Aranda, Jesus; Universidad Del Valle, Cali, Colombia
CORDY, Maxime ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SerVal
Ortiz, James; University of Namur, FOCUS/NaDI, Namur, Belgium
Perrouin, Gilles; University of Namur, PReCISE/NaDI, Namur, Belgium
Schobbens, Pierre-Yves; University of Namur, PReCISE/NaDI, Namur, Belgium
External co-authors :
yes
Language :
English
Title :
MUPPAAL: Reducing and Removing Equivalent and Duplicate Mutants in UPPAAL
Publication date :
16 April 2023
Event name :
2023 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)
Event place :
Dublin, Irl
Event date :
16-04-2023 => 20-04-2023
Main work title :
Proceedings - 2023 IEEE 16th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2023
Publisher :
Institute of Electrical and Electronics Engineers Inc.
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. We thank Paul Temple for the early discussions on this work.ACKNOWLEDGMENT 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. We thank Paul Temple for the early discussions on this work.
B. K. Aichernig, J. Auer, E. Jobstl, R. Korosec, W. Krenn, R. Schlick, and B. V. Schmidt. Model-based mutation testing of an industrial measurement device. In Tests and Proofs, volume 8570 of LNCS, pages 1-19. Springer, 2014.
B. K. Aichernig, F. Lorber, and D. Nickovic. Time for mutants - model-based mutation testing with timed automata. In M. Veanes and L. Vigaǹo, editors, Tests and Proofs - 7th International Conference, TAP 2013, Budapest, Hungary, June 16-20, 2013. Proceedings, volume 7942 of Lecture Notes in Computer Science, pages 20-38. Springer, 2013.
R. Alur and D. L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183-235, 1994.
R. Alur, T. A. Henzinger, and M. Y. Vardi. Parametric real-time reasoning. In STOC, pages 592-601. ACM, 1993.
D. Basile, M. H. t. Beek, S. Lazreg, M. Cordy, and A. Legay. Static detection of equivalent mutants in real-time model-based mutation testing. Empirical Software Engineering, 27(7):160, 2022.
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 R. E. Lopez-Herrejon, editor, SPLC ’20: 24th ACM International Systems and Software Product Line Conference, Montreal, Quebec, Canada, October 19-23, 2020, Volume A, pages 30:1–30:11. ACM, 2020.
G. Behrmann, A. David, and K. G. Larsen. A tutorial on UPPAAL. In M. Bernardo and F. Corradini, editors, 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, number 3185 in LNCS, pages 200-236. Springer-Verlag, September 2004.
M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: a model-checking tool for real-time systems. In Hu, A. J. Vardi, and M. Y., editors, Computer Aided Verification 10th International Conference, CAV'98, volume 1427 of Lecture Notes in Computer Science, pages 546-549, Vancouver, BC, Canada, June 1998.
T. A. Budd and A. S. Gopal. Program testing by specification mutation. Computer Languages, 10(1):63-73, Jan. 1985.
K. Cer¯ans. Decidability of bisimulation equivalences for parallel timer processes. In G. von Bochmann and D. K. Probst, editors, Proceedings of the 4th International Workshop on Computer Aided Verification (CAV'92), volume 663 of Lecture Notes in Computer Science, pages 302-315. Springer-Verlag, 1993.
A. David, K. Larsen, A. Legay, U. Nyman, and A. Wasowski. Ecdar: An environment for compositional design and analysis of real time systems. In Lecture Notes in Computer Science, volume 6252/2010, Germany, 2010.
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, pages 91-100, New York, NY, USA, 2010. ACM.
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, 2018.
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, pages 210-, Washington, DC, USA, 1999.
G. Fraser and A. Arcuri. Achieving scalable mutation-based generation of whole test suites. Empirical Software Engineering, pages 1-30, 2014.
K. Guldstrand Larsen, M. Mikucionis, and B. Nielsen. Uppaal tron user manual - docs.uppaal.org, Jun 2017.
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:147-160, Sep 2018.
T. A. Henzinger, P.-H. Ho, and H. Wong-toi. Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1:460-463, 1997.
A. Hessel and P. Pettersson. Cover-A test-case generation tool for timed systems. Testing of software and communicating systems, pages 31-34, 2007.
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, pages 660-669, Los Alamitos, CA, USA, jul 2012.
W. E. Howden. Reliability of the path analysis testing strategy. IEEE Transactions on Software Engineering, 2(3):208-215, 1976.
H. Jensen, K. Larsen, and A. Skou. Modelling and analysis of a collision avoidance protocol using spin and uppaal. BRICS Report Series, 3, 01 2002.
Y. Jia and M. Harman. An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng., 37(5):649-678, Sept. 2011.
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, pages 654-665, Hong Kong, Nov. 2014.
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.
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 M. Nunez and M. Gudemann, editors, Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings, volume 9128 of Lecture Notes in Computer Science, pages 47-61. Springer, 2015.
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, pages 142-151. IEEE Computer Society, 2016.
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), pages 319-328, March 2017.
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, pages 299 - 306. ACM Press New York, NY, USA, September 18-22 2005.
M. Lindahl, P. Pettersson, and W. Yi. Formal design and analysis of a gear controller. International Journal on Software Tools for Technology Transfer, 3(3):353-368, Aug 2001.
L. Madeyski, W. Orzeszyna, R. Torkar, and M. Jozala. Overcoming the equivalent mutant problem: A systematic literature review and a comparative experiment of second order mutation. IEEE Trans. Software Eng., 40(1):23-42, 2014.
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 - Volume 01, COMPSAC '04, pages 306-311, Washington, DC, USA, 2004.
J. Offutt. A mutation carol: Past, present and future. Information and Software Technology, 53(10):1098-1107, Oct. 2011.
J. J. Ortiz, M. Amrani, and P. Schobbens. Multi-timed bisimulation for distributed timed automata. In C. Barrett, M. Davies, and T. Kahsai, editors, NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings, volume 10227 of Lecture Notes in Computer Science, pages 52-67, 2017.
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, pages 936-946. IEEE, 2015.
M. Papadakis, M. Kintis, J. Zhang, Y. Jia, Y. L. Traon, and M. Harman. Mutation testing advances: An analysis and survey. Advances in Computers, 112, 2018.
M. Papadakis and N. Malevris. Automatic mutation test case generation via dynamic symbolic execution. In ISSRE, pages 121-130. IEEE, 2010.
T. Parr. The Definitive ANTLR 4 Reference. Pragmatic Bookshelf, Raleigh, NC, 2 edition, 2013.
F. Siavashi, J. Iqbal, D. Truscan, and J. Vain. Testing Web Services with Model-Based Mutation, page 45-67. Springer, 2017.
J. Tretmans. Formal Methods and Testing - An Outcome of the FORTEST Network (Revised Papers Selection), chapter Model Based Testing with Labelled Transition Systems, pages 1-38. Springer-Verlag, 2008.
J. J. O. Vega, G. Perrouin, M. Amrani, and P.-Y. Schobbens. Modelbased mutation operators for timed systems: A taxonomy and research agenda. 2018 IEEE International Conference on Software Quality, Reliability and Security (QRS), 2018.
J. M. Voas and G. McGraw. Software Fault Injection: Inoculating Programs Against Errors. John Wiley & Sons, Inc., 1997.
J. Zander, I. Schieferdecker, and P. J. Mosterman. Model-Based Testing for Embedded Systems. CRC Press, 2017.
