Information Technology Reference
In-Depth Information
Mutation-Based Test Case Generation for
Simulink Models
Angelo Brillout
1
, Nannan He
2
, Michele Mazzucchi
1
, Daniel Kroening
2
,
Mitra Purandare
1
, Philipp Rummer
2
, and Georg Weissenbacher
1
,
2
1
Computer Systems Institute, ETH Zurich
2
Computing Laboratory, Oxford University
Abstract.
The Matlab/Simulink language has become the standard for-
malism for modeling and implementing control software in areas like
avionics, automotive, railway, and process automation. Such software is
often safety critical, and bugs have potentially disastrous consequences
for people and material involved. We define a verification methodology
to assess the correctness of Simulink programs by means of automated
test-case generation. In the style of fault- and mutation-based testing,
the coverage of a Simulink program by a test suite is defined in terms
of the detection of injected faults. Using bounded model checking tech-
niques, we are able to effectively and automatically compute test suites
for given fault models. Several optimisations are discussed to make the
approach practical for realistic Simulink programs and fault models, and
to obtain accurate coverage measures.
1
Introduction
Model-based design is a development methodology for modern software artifacts.
It promotes the use of powerful and specialized modeling languages, allowing the
engineer to focus on the domain-specific aspects of the system under develop-
ment. The implementation of the system is either generated or derived manually
from high-level models. The goal is to identify design flaws as early as possible
in the development cycle, thereby avoiding costly late-stage design fixes.
The Matlab/Simulink language, developed by The MathWorks,
1
has emerged
as the predominant modeling formalism in the automotive industry and is also
widely deployed for avionic applications. A software glitch in these application
domains may result in high cost and considerable damage of reputation. Due to
the safety-critical nature of these domains, defects in the software may put hu-
man lives at stake. Accordingly, international safety standards such as DO-178B
or IEC 61508 demand the application of rigorous verification techniques. In par-
ticular, they require the test engineers to provide a set of test cases that exercise
the implementation of the system according to certain coverage metrics. The
Supported by the EU FP7 STREP MOGENTES (project ID ICT-216679) and the
ARTEMIS CESAR project.
1
http://www.mathworks.com/products/simulink/
