Information Technology Reference
In-Depth Information
effort to create appropriate test suites is substantial, and the execution of the
test suites is time consuming. There is therefore a strong incentive to automate
the generation of test cases and to keep the resulting test suite small.
Model-based testing is an application of model-based design for deriving test
cases from a model of the design, which promises better scalability and is applica-
ble before the implementation phase. In the context of model-based testing, the
question of suitable coverage metrics has to be reconsidered: traditional metrics
such as location or branch coverage are no longer meaningful, since the test cases
are not derived from implementation source code. In this paper, we focus on mu-
tation testing : the quality of the test suite is assessed by injecting mutations into
the model and by measuring which percentage of these modifications can be de-
tected when exercising the test cases. We say that a modification is detected if we
can observe that the modified and the original model generate different output
signals. The resulting test vectors can be used to check that the model satisfies
requirements or can be applied to an implementation of the design.
The generation of test suites that achieve high mutation coverage is dicult.
We use model checking [1] for this task, as it is also able to address the issue of
equivalent mutants . The application of model checking to generate high-coverage
test suites has become commonplace (see, for instance, [2] for an application in
the automotive domain). Test case generation for Simulink models is complicated
by the fact that the Simulink language lacks a formal semantics and makes heavy
use of floating-point arithmetic.
Contribution. We describe an application of the bounded model checking engine
Cbmc [3] to generate test suites for Simulink models with high mutation coverage.
The implementation features precise reasoning with respect to the floating-point
semantics of the models. The computational complexity of the underlying model
checking algorithm requires us to deploy a number of heuristics to achieve the
desired coverage if the number of mutations is large. Moreover, these heuristics
also serve the orthogonal purpose of keeping the number of redundant test cases
small in order to reduce the time required to execute the test suite.
Related Work. We briefly relate our work to other tools that generate test-
vectors by means of software model checkers. A number of papers report appli-
cations of Cbmc or similar techniques for generating high-coverage test suites
[4,5,6]. These implementations are very similar to ours. There are also reports
of the use of predicate abstraction in test-vector generation, e.g., using Slam [7]
and Blast [8].
We refer the reader to [9] for a broad survey on mutation testing. We only con-
sider mutant models with single mutations, whereas other authors also consider
combinations of faults [10]. Do and Rothermel [11] proposes to use mutations to
prioritise test cases to increase a test suite's rate of fault detection.
Schuler et al. [12] discusses the impact of equivalent mutations (mutations
that keep the semantics of the model unchanged) and presents an approach to
detect such mutations by means of checking dynamic invariants. We propose a
similar approach in Section 5, but we rely on invariants statically generated by
means of verification techniques such as k -induction.
 
Search WWH ::




Custom Search