Mapping UML to Labeled Transition Systems for Test-Case Generation - Formal Methods for Components and Objects - page 240

However, even with this assumptions there is a fundamental diculty in this
approach. Not all mutations represent actual faults producing observable failures.
For example, a mutation in dead code, i.e., code that is never executed, will not
lead to failures. Mutants with such an equivalent behavior are called equivalent
mutants and can never be killed by any test case. This posed a serious limitation
to the mutation testing technique: for a mutant surviving the tests, i.e., it is not
killed, we do not know if this is due to our inability to come up with a proper
test case or due to the fact that there is no such test case. Unfortunately, the
problem is undecidable in general.
In recent years, however, with the advent of model checking techniques, the
situation improved considerably: Today, the equivalence of two mutants can be
decided for a growing class of programs assuming finite datatypes. This may
explain the returning interest in mutation testing. For abstract models of a SUT
the situation is even better. We have implemented such an equivalence checker,
more precisely a conformance checker, for deciding if two action systems are
equivalent. In case of non-equivalence (non-conformance) we generate a discrim-
inating test case.
Hence, in model-based mutation testing we mutate the models of a SUT and
generate test cases that would kill an implementation of a mutated model. The
test cases are generated with the help of a conformance checker. In the following,
we describe this test case generation technique in more detail.
5.2 Test Case Generation via Conformance Checking
As explained above, conformance or equivalence checking is at the heart of
our test case generation technique. The reason why we prefer the term con-
formance checking to equivalence checking is the fact that our models are non-
deterministic. Therefore, conformance is formally a pre-order relation, but not
an equivalence relation.
In testing, we are only interested in external events. By interpreting our action
systems in terms of their labeled actions, we map qualitative action systems to a
labeled transition system (LTS) semantics. Furthermore, we distinguish between
controllable (input), observable (output), and internal ( τ ) actions. Based on
this LTS semantics we apply the input-output conformance relation ioco [17]
for generating mutation-based test cases. Therefore we implemented an ioco
checker in SICStus Prolog 1 which verifies the conformance between two given
qualitative action systems by computing the synchronous product modulo ioco
[6]. The result of the check is again an LTS which, in the case of non-conformance,
contains fail states. These fail states are then used in the step of test case
extraction to obtain test cases which reveal the mutated behavior.
The ioco relation states that for all suspension traces in the specification
the outputs of the implementation after such a trace must be allowed in the
specification after the same trace. Here, suspension traces are traces of the spec-
ification over inputs, outputs, and quiescence. These traces are obtained from a
1 http://www.sics.se/sicstus/