Mutation Testing with Hyperproperties

Autor: Andreas Fellner, Mitra Tabaei Befrouei, Georg Weissenbacher
Rok vydání: 2019
Předmět:
Zdroj: Software Engineering and Formal Methods ISBN: 9783030304454
SEFM
Software Engineering and Formal Methods-17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings
Software and Systems Modeling
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Software Engineering and Formal Methods
ISSN: 0302-9743
1611-3349
DOI: 10.1007/978-3-030-30446-1_11
Popis: We present a new method for model-based mutation-driven test case generation. Mutants are generated by making small syntactical modifications to the model or source code of the system under test. A test case kills a mutant if the behavior of the mutant deviates from the original system when running the test. In this work, we use hyperproperties-which allow to express relations between multiple executions-to formalize different notions of killing for both deterministic as well as non-deterministic models. The resulting hyperproperties are universal in the sense that they apply to arbitrary reactive models and mutants. Moreover, an off-the-shelf model checking tool for hyperproperties can be used to generate test cases. We evaluate our approach on a number of models expressed in two different modeling languages by generating tests using a state-of-the-art mutation testing tool.
To appear at the international conference of software engineering and formal methods
Databáze: OpenAIRE