# Mutation Testing with Hyperproperties

## TL;DR

This paper introduces a novel mutation testing approach using hyperproperties to formalize and generate test cases for both deterministic and non-deterministic reactive models, leveraging existing model checking tools.

## Contribution

It presents a new method that formalizes mutation testing with hyperproperties, enabling test generation for arbitrary reactive models and mutants.

## Key findings

- Applicable to deterministic and non-deterministic models
- Uses existing hyperproperty model checking tools
- Effective in generating mutation-based test cases

## Abstract

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.