Information Technology Reference
In-Depth Information
5 Detecting Non-observability of Mutations
In traditional mutation-based testing, the di
culty to identify mutations without
observable effect on the system outputs is known to be one of the main obstacles.
Assume that one instance
EQ
k
∧
F
c
of (4) (with
i
=
c
) is unsatisfiable. This
indicates that the injected fault corresponding to
f
c
(see Formula (2)) does not
result in an error that propagates to an observable output within
k
steps. There
are two possible reasons for this phenomenon:
1. The bound
k
is not suciently large to reveal the error.
2. The model contains redundancy and the injected fault does not result in an
observable change of its behavior. We say that the model
tolerates
the fault.
The mutant is an
equivalent mutant
.
A
complete
model checking algorithm can distinguish both cases. The first case
can be addressed by simply increasing the bound
k
. In the second case, the
mutation is not
strong
enough to have any impact on the observable behavior
of the model and the model checking tool provides a
proof
for the equivalence
of the mutated and original model. This concept is explained in the following
subsection.
5.1
Model Checking, Induction, and Invariants
BMC is only capable of providing a guarantee that a property
P
is not violated
within at most
k
execution steps. In this section, we briefly discuss two techniques
to lift this restriction:
k
-induction [28] and finding invariants by means of fixed-
point detection [1].
k
-Induction.
This technique generalizes the standard induction principle, and
has been used before for test-vector generation for Simulink models [2]. The base
case is established by means of BMC. The following equation holds if and only
if the property
P
is not violated in the first
k
execution steps:
k−
1
k
I
(
s
0
)
∧
R
(
s
i
,s
i
+1
)
∧
P
(
s
i
)
(6)
i
=0
i
=0
If the base case (6) holds, the technique proceeds to show by induction that
P
holds for any arbitrary
k
∈
:
⎛
⎞
k
k
⎝
⎠
⇒
R
(
s
i
,s
i
+1
)
∧
P
(
s
j
)
P
(
s
k
+1
)
(7)
i
=0
j
=0
Formula (6) in combination with (7) implies that the sequence of states can be
extended to a path of arbitrary length without ever violating
P
.Thus,ifwecan
find a
k
for which the conjunction of (6) and (7) holds, then the model is safe.
To check whether this conjunction holds for a given
k
,werelyonecient
decision procedures (SAT solvers such as [27], in particular). Let
G
=(6)
∧
(7). If
