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

Depending on the extent of these modifications, the resulting error may not
be immediately observable, i.e., it is not necessarily the case that

s 0 .i = s 0 .i R ( s 0 ,s 1 )= = s 1 .o

∧ R ( s 0 ,s 1 ) ∧ ⇒ s 1 .o

holds. Even though s 1 differs from s 1 , the outputs s 1 .o and s 1 .o may be indis-
tinguishable: the modification of R may not necessarily have an (immediate)
impact on the observable behavior. Intuitively, a test case is “good” if it yields
a different outcome for M and M . In mutation testing, the term weak mutation
testing refers to the condition that the test cases should cause different program
states for the mutant and the original model. In the case that the affected part
of the state is not observable, this condition is not sucient for our purpose.
Strong mutation testing refers to the case where the error propagates to the
output of the model and is caught by an appropriate test case. In dependable
systems, this notion may be too strong, since redundant systems may tolerate a
certain number of faults. Note that this case can be detected using a complete
model checking technique or k -induction. A brief outline of these techniques is
provided in Section 5.1.

3.6 Generating Test Cases

One way of generating test cases that detect a mutation is to find a satisfying
assignment to Formula (1). Such a satisfying assignment provides the inputs
that yield a different output sequence during the first k steps and, provided the
observable behaviors of the two models M and M are not fully equivalent, such
a solution must exist for some k .

Encoding Combinations of Faults. Assume that the objective is to gener-
ate a test suite that detects single faults (or mutations). The na ıve approach
to create such a test suite is to generate a new model M for each conceivable
fault or mutation and to generate an instance of Formula (1) for each pair of
models M and M . In practice, this approach is very wasteful, since modern
satisfiability checkers such as MiniSAT [27] are able to solve problem instances
incrementally .Encoding M in a way such that faults or mutations can be acti-
vated or deactivated by adding constraints to the formula allows the SAT solver
to (partially) reuse the information it has already derived.
Therefore, we propose to generate a modified model M that contains all faults
and mutations for which we want to generate test cases. We use the same idea
as in Figure 4b and introduce a Boolean flag f for each modification that allows
us to activate (deactivate) the respective fault/mutation by setting f to true
(false). Assume that R is the transition relation of the original model M and
that R i is the transition relation of the model M i that contains the i th of the n
modifications in question. We define the model R μ as follows: