Information Technology Reference
In-Depth Information
Example 4 shows that it is not always the case that a test-case that detects
a combination of mutations and faults also covers each mutation independently.
While we have found a test vector
t
=
which “kills”
the mutation, the same test vector fails to cover the fault. We are forced to
generate an additional test case for the injected fault, which can be achieved by
deactivating the enable flag for the fault and starting another incremental run
of the SAT solver.
We propose to analyze the model systematically, starting with a set of muta-
tions
T
. The corresponding algorithm is outlined in Figure 6. We generate a test
case which covers this set of mutations
T
and check whether it independently
covers the single elements of
T
. The advantage of the algorithm is that it is
possible to prune entire subsets of mutations if
C
in step
{
i
1
→
0
.
0
,i
2
→
23
.
4
}
is non-empty. If this
is not the case, we have to split
T
recursively. In the worst case, we still require
n
test-cases to cover all
n
mutations.
➂
Input:
A model and a set of mutations
T
Output:
Atest-suite
S
covering the mutations in
T
.
➀
If
T
=
∅
, terminate.
Compute a test case
t
satisfying
EQ
k
∧ F
T
➁
(as defined in (5)).
(
C
=
∅
if there is no such
t
).
➂
Let
C ⊆ T
be the set of mutations independently covered by
t
:
➊
If
C
=
∅
,let
T
:=
T \ C
.Add
t
to the test suite and proceed to
➀
.
➋
If
C
=
∅
, partition
T
into
T
1
and
T
2
s.t.
T
=
T
1
∪T
2
,and
T
1
∩T
2
=
∅
.
Call the algorithm recursively with
T
:=
T
1
and
T
:=
T
2
, respectively.
Fig. 6.
An algorithm for systematic test-case generation
The success or failure of this approach depends inherently on the structure of
the mutations and the model
M
. In the following, let
ν
1
and
ν
2
be two mutations
for
M
. Furthermore, let
s
0
,...,s
n
be an execution trace of
M
,and
s
0
,...,s
n
be
an execution trace of
M
with both mutations enabled.
Assume that
ν
1
and
ν
2
affect different output signals, i.e., given a fixed input
sequence
s
0
.i,...s
n
.i
, the set of signals changed by activating the mutation
ν
1
is disjoint from the set of signals changed by enabling the mutation
ν
2
. Then,
we can increase the chance of finding a test case that covers both mutations
independently by trying to maximize the difference between
s
0
.o,...s
n
.o
and
s
0
.o,...s
n
.o
.
Unfortunately, such an independence cannot be assumed in general, since
there may be a mutual influence between mutations. In particular, two mutations
may cancel each other out. Checking whether two mutations are independent in
the sense explained above is computationally as expensive as model checking
and therefore not a feasible strategy.
