Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar

TL;DR

This paper presents an extension of the Ecdar model checker that integrates conformance testing with model-based mutation testing, enabling efficient fault detection and localization in real-time systems within an IDE.

Contribution

It introduces a new IDE for Ecdar that combines modeling, verification, and testing, with novel mutation operators and parallelized testing for real-time systems.

Findings

Ecdar detects all faults in a case study with 140 faulty systems.

The tool supports real-time and simulated time testing.

Parallel test execution significantly speeds up the process.

Abstract

Model checking of real-time systems has evolved throughout the years. Recently, the model checker Ecdar, using timed I/O automata, was used to perform compositional verification. However, in order to fully integrate model checking of real-time systems into industrial development, we need a productive and reliable way to test if such a system conforms to its corresponding model. Hence, we present an extension of Ecdar that integrates conformance testing into a new IDE that now features modelling, verification, and testing. The new tool uses model-based mutation testing, requiring only the model and the system under test, to locate faults and to prove the absence of certain types of faults. It supports testing using either real-time or simulated time. It parallelises test-case generation and test execution to provide a significant speed-up. We also introduce new mutation operators that improve the ability to detect and locate faults. Finally, we conduct a case study with 140 faulty systems, where Ecdar detects all faults.