TChecker Mutation

Enhanced mutation testing support for TChecker, the open source model checker for timed automata and timed automata networks.

Overview

Mutation testing is a powerful technique to generate test cases for your system.
Potential errors in your system can be modelled by introducing controlled modifications (mutants) into timed automata models — such as altering clocks, guards and synchronisation.
Test inputs that cause a mutant to behave differently from the original automaton can serve as a test case to find similar errors.
TChecker Mutation provides efficient support for identifying such distinguishing test cases based on TChecker.

Features

TChecker Mutation generates mutations of timed automata networks by modifying their structure, clock constraints (guards and invariants), clock resets, event synchronisations and more. In particular, the following operators for mutation generation are implemented:

• all

Attribute changing:

• change_event (from [1])
• change_constraint_cmp (inspired by [1])
• change_constraint_clock
• decrease_constraint_constant (from [2])
• increase_constraint_constant (from [2])
• invert_committed_location (from [3])
• invert_reset (from [1])
• invert_urgent_location (from [3])
• negate_guard (from [1])

Structure changing:

• add_location (from [1])
• add_transition (from [2])
• change_transition_source (from [1])
• change_transition_target (from [1])
• remove_location (from [2])
• remove_transition (from [2])

Synchronisation changing:

• add_sync (inspired by [3])
• add_sync_constraint (inspired by [3])
• change_sync_event (inspired by [3])
• invert_sync_weakness (inspired by [3])
• remove_sync (inspired by [3])
• remove_sync_constraint (inspired by [3])

For operator option all, all possible mutations for each implemented operator are generated.
For operator options decrease_constraint_constant, increase_constraint_constant and all, an optional integer value to decrease/increase constants by can be specified. Default is 1.

Prerequisites

Before using TChecker Mutation, install the required dependencies:

pip install -r requirements.txt 

Usage

To generate mutations, run the following command:

python mutate.py --in_ta <input_tchecker_file> --out_dir <output_directory> --op <operator> [--val <int>]

For example:

python mutate.py --in_ta ad94.tck --out_dir out --op remove_location

The input file must be a .txt or .tck file in valid TChecker syntax.
For a given network of timed automata, every possible mutation is generated with the specified operator and written as a .tck file in the specified output directory.
Mutations that are bisimilar to the original network are written to a seperate directory bisimilar_mutations inside the output directory.
Whether a mutation is bisimilar or not is logged in bisimilarity_log.csv in bisimilar_mutations.

Note: Output mutation files do not preserve comments of the original TChecker file.

Literature

1. B. K. Aichernig, F. Lorber and D. Ničković. Time for Mutants - Model-Based Mutation Testing with Timed Automata (2013)
2. D. Basile, M. H. ter Beek, S. Lazreg, M. Cordy, A. Legay. Static detection of equivalent mutants in real-time model-based mutation testing (2022)
3. D. Cortés, J. Ortiz, D. Basile, J. Aranda, G. Perrouin, P. Schobbens. Time for Networks: Mutation Testing for Timed Automata Networks (2024)