Information Technology Reference
In-Depth Information
⎧
⎨
R
(
s
0
,s
1
)if
n
i
=1
f
i
=
F
R
1
(
s
0
,s
1
) f
f
1
=
T
∧
=2
f
i
=
F
∧
=3
f
i
=
F
R
2
(
s
0
,s
1
) f
f
2
=
T
f
1
=
F
∧
R
μ
(
s
0
,s
1
,f
1
,...,f
n
):=
(2)
.
R
n
(
s
0
,s
1
) f
f
n
=
T
⎩
n−
1
=1
f
i
=
F
∧
We use
M
μ
to denote the model with the transition relation
R
μ
.
Given the resulting transition relation
R
μ
(as defined in (2)) we can construct
an instance of Formula (1). A fault in the modified model
M
μ
can be triggered
by adding a constraint of the form
F
j
:=
f
j
f
i
.
∧
¬
(3)
0
<i≤n,i
=
j
Example 2.
Figure 5 shows a mutation and a fault injected into the Simulink
diagram in Figure 4a. The first diagram shows the implementation of a signal-
stuck-at-0 fault. The diagram below combines this fault and the mutation in
Figure 4b into one model. The model provides two flags allowing us to trigger
the mutations.
The decision procedure of Cbmc, the model checker which our test case gener-
ation tool Cover is based on, performs bit-level accurate reasoning by trans-
forming the instance of Formula (1) into an equi-satisfiable propositional formula
EQ
k
in Conjunctive Normal Form
2
(CNF). This formula is then handed over
to the satisfiability checker MiniSAT [27]. The decision process of MiniSAT is
incremental, i.e., it allows
-
to add additional clauses, and
-
to add or remove a constraint
F
j
of the form described in (3)
without reinitializing
the solver, meaning that the solver can reuse intermediate
results if it has to solve similar problem instances.
Let
EQ
k
denote the CNF of the instance of Equation (1) derived from the
models
M
and
M
μ
. We can generate a test suite covering all
n
mutations in
question by iteratively computing satisfiable assignments to
F
i
,
EQ
k
∧
i
∈{
1
,...,n
}
.
(4)
We say that a test case
t
independently
covers a mutation if it corresponds to
a satisfying assignment of (4) for that mutation
i
. If each of the instances of
Formula (4) has a solution, we obtain
n
(not necessarily different) test cases
that cover all mutations injected into the model
M
μ
.
2
A propositional formula in conjunctive normal form is a conjunction of disjunctions
of literals, where a literal
l
is a propositional variable or its negation (e.g.,
a
or
¬a
).
A
clause
is a disjunction of literals.
