Starkes modellbasiertes Mutationstesten

Abstract

Powerful verification and validation methods are needed to keep up with the complexity of modern systems. While testing remains the most prevalent verification and validation method, scaling testing to huge and interdependent systems poses a big challenge. We address this challenge by presenting scalable methods for model-based mutation testing with a focus on strong mutation and non-deterministic models of concurrent reactive systems. Model-based testing aims to automatically create test cases from a model of some system under test. We use mutations as the driving criterion in model-based test generation. Strong mutation analysis aims to reveal differences in the output of a model and mutations of it via test cases. Mutations mimic implementation errors and a key assumption of mutation testing is that the ability of a test suite to reveal artificial errors carries over to its ability to reveal actual faults. We establish a rigorous theoretical framework for strong model-based mutation testing in presence of non-determinism. We embedded this framework into the theory of hyperproperties, which enables mutation testing via hyperproperty model checking and thus rigorous mutation analysis. Furthermore, we propose an explicit state and exploration-based test case generation algorithm that is tuned for scalability. It executes mutants lazily and explores state spaces in a branching search manner. Finally, we enable test case generation for highly concurrent models by connecting this algorithm with event structure-based partial order reduction. To this end, we map strong killing onto a language inclusion problem over event structures, prove the computational complexity of this problem, provide a decision algorithm for it, and obtain a novel type of test cases that incorporates the concurrent behavior of the model.