  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.
