Information Technology Reference
In-Depth Information
Fig. 11.
Adaptive example test case for our two-tank system. For the sake of simplicity,
qual
events are internal, i.e., not visible.
7 Concluding Remarks
We have presented two key abstractions for testing a hybrid system: action sys-
tems and qualitative differential equations. The core of the paper covers our tool-
supported mutation testing approach including empirical results of the running
example. In addition, we have discussed the different possibilities for selecting
test cases.
To our knowledge this is the first work on model-based mutation testing for
hybrid systems. The modeling formalism [2] and the conformance checker [6]
have been published previously, but the testing approach is a new contribution
of this paper. Furthermore, we added parameters to the qualitative events to
guarantee controllability. The idea of model-based mutation testing can be traced
back to Budd and Gopal, who mutated specifications in the form of predicate
calculus [7]. For a thorough overview of related work on model-based mutation
testing we refer to our theory paper on mutation testing [4]. With respect to
the LTS interpretation of action systems our work is close to other integrated
approaches combining state-based modeling languages and process algebras, e.g.,
[8]. The
B
model specifies the abstract state and the operations of the system
while the
CSP
model describes the order in which the operations occur. The
combined semantics is a parallel composition of the models which synchronize
on common operations (events). This combination of B [1] and CSP [12] has
been implemented in the
ProB
tool [14], a model checker and animator for B
that can also check for CSP's notions of (event) refinement.
ProB
also relates
to our conformance checker from an implementation point of view: both are
implemented in SICStus Prolog. Finally, with respect to hybrid system analysis,
we refer to Henzinger's work on hybrid automata [11]. However, our extension
of action systems was mainly inspired by Ronkk¨oetal.[16].
The test case generation process via conformance checking between a speci-
fication and a mutant is costly. Therefore, in practise we delay this process as
long as possible. We start with a set of randomly generated test cases and run
