Information Technology Reference
In-Depth Information
numbers. If the model is implemented and executed using floating-point num-
bers, however, the stream of sums
t
1
,t
2
,t
3
,...
will eventually get stationary due
to lack of precision: in FPA, it is the case that
a
+
b
=
a
if
a
is a very large and
b
a very small number. As soon as
t
n
=
t
n−
1
occurs in the sequence of sums, the
computation of the quotient will raise a division-by-zero exception.
The use of a bit-accurate decision procedure has further advantages in the
context of mutation testing: Many fault models are based on bit-level modifica-
tions (such as
single-bit-stuck-at
faults). The effect of these mutations is trivial to
model using a propositional formula, and SAT-solvers can deal with the resulting
encoding very eciently. For instance, modeling a single-bit-stuck-at-1 fault cor-
responds to setting a single propositional variable to true. Modern SAT-solving
algorithms deal with this case by using unit propagation, which is extremely
ecient. If, on the other hand, a decision procedure for reasoning about real
arithmetic was used, encoding the same fault would be complicated and would
result in constraints that are very hard to solve.
3.5
Mutation Testing and Fault Injection
From an abstract point of view, mutations as well as injected faults are simply
modifications to the behavior of the model.
Example 1.
Consider the simple Simulink diagram in Figure 4a. The input sig-
nals
i
1
and
i
2
are related to the output signal
o
by means of the formula
o
=
i
1
×
i
2
, i.e., the transition function is
R
(
s
i
,s
i
+1
)
de
=
s
i
.o
=
s
i
.i
1
×
s
i
.i
2
∧
s
i
+1
.o
=
s
i
+1
.i
1
×
s
i
+1
.i
2
.
A possible syntactic mutation is to replace the multiplication (
×
)withan
addition:
R
(
s
i
,s
i
+1
)
de
=
s
i
.o
=
s
i
.i
1
+
s
i
.i
2
∧
s
i
+1
.o
=
s
i
+1
.i
1
+
s
i
+1
.i
2
.
This mutation can be implemented in the diagram using an
enable
signal, al-
lowing us to switch the mutation on and off (see Figure 4b).
In our formalism, such a modification can be modeled by replacing the tran-
sition relation
R
of our model
M
with a slightly modified transition relation
R
(and possibly a modified condition
I
for the initial state). The faults introduced
into the system may be either permanent, transient, or intermittent (i.e., occur
repeatedly). The former case can be simply modeled by permanently altering
the transition relation
R
, and applying the resulting relation
R
in each step:
I
(
s
0
)
R
(
s
0
,s
1
)
R
(
s
1
,s
2
)
R
(
s
2
,s
3
)
R
(
s
3
,s
4
)
∧
∧
∧
∧
∧
...
permanent fault
To model transient or intermittent faults, we have to take the temporal aspect
into account, i.e., the alteration becomes only effective at certain points in time.
