Model-Based Mutation Testing of Real-Time Systems via Model Checking

Model-based mutation testing is a fault-based technique for generating effective test suites. Given a formal model of a system and a set of slightly altered variants of the model (mutants), the approach generates a test suite that is able to distinguish the original model from all (non-equivalent) mutants. Generally, this is done via conformance checks between the mutants and the correct specification where witness traces of non-conformance are transformed into test cases. While this procedure generates high-quality test suites, the conformance checks are computationally expensive, resulting in a high test-case generation time. To ensure that the specification is correct, many safety-critical systems are additionally specified via properties, e.g., timed computation tree logic (TCTL) properties. These can be used to verify the specification model via model checking. After this check, the properties are often not used any further. In this paper, we propose to reuse the properties in a combination of model-based mutation testing and the model-checking of properties for real-time systems. That is, we generate a set of mutated models, and check whether they still satisfy the specified properties. In case of a violation, we receive a trace to this violation, which can be transformed into a test case in the same way as in the traditional approach. The advantages of the approach are manifold: the checking of individual small properties is often more efficient than a full conformance check; the resulting test suite is smaller in size and mainly focuses on the safety-critical parts that were specified by the properties; the distribution of the generated test cases gives a very good indication on the quality of the properties; the technique can also be applied to certain kinds of non-functional properties. We apply the technique to an industrial case study of an automated gear controller. It is modeled as a network of timed automata and specified via 46 TCTL properties. We use the tool UPPAAL and its model-checking capabilities to demonstrate the approach.