Information Technology Reference
In-Depth Information
The following theorem states that those mutations that do not appear in the final
proof of
G
= (10)
(11) checked during
k
-induction are non-observable [31].
Theorem 1.
A mutation corresponding to an enabling variable
f
j
∧
that does not
appear in the final proof of
G
is unobservable.
Proof.
A variable absent in the proof does not influence the conclusion of the
proof. Thus, enabling a flag
f
j
absent in the proof does not invalidate the proof
of
k
-inductivity and hence, does not break equivalence.
Thus, mutations absent in the proof do not need to be checked as these are
unobservable.
Inductive Invariant.
An inductive invariant represents a set of safe states with
respect to a certain property of the model. Consider the composition of the
two models
M
and
M
o
(where
i.
(
s
i
.i
=
s
i
.i
)) and let
i.
(
s
i
.o
=
s
i
.o
)bethe
∀
∀
property in question.
Theorem 2.
Let
J
(
s, s
)
represent an invariant over the state space of the two
models that warrants the equivalence of
M
and
M
o
, i.e., that
i.J
(
s
i
,s
i
)
⇒
(
s
i
.o
=
s
i
.o
)
holds. Furthermore, let
R
be the transition function of
M
o
,only
that the
j
th
mutation is enabled (
f
j
=
∀
T
). If
I
(
s
0
)
J
(
s
0
,s
0
)
and
J
(
s
i
,s
i
)
I
(
s
0
)
∧
⇒
R
(
s
i
,s
i
+1
)
J
(
s
i
+1
,s
i
+1
)
∧
R
(
s
i
,s
i
+1
)
∧
⇒
holds, then the
j
th
mutation is unobservable.
Proof.
The inductive invariant
J
is also an inductive invariant of the resulting
mutated system and therefore establishes equivalence.
6Con lu on
We have defined a methodology for automated test case generation for Simulink
models. By formulating test coverage and goals in terms of fault models, we
achieve a flexible and general framework that subsumes standard coverage crite-
ria and is directly related to functional and non-functional requirements specifi-
cations. The use of equivalence checking and bounded model checking makes it
possible to explore the behavior of models with high precision, taking intricate
details such as the actual floating-point semantics of execution platforms into
account. We implemented this approach in our test-case generation tool Cover,
which is based on the model checker Cbmc. The evaluation of Cover on indus-
trial case studies developed in the European projects MOGENTES and CESAR
is currently in progress.
In order to handle the size of real-world Simulink models, we have introduced
two main concepts to keep the complexity of test case generation manageable:
a strategy to compute small test suites by maximizing the number of mutations
that are covered by each test case, and techniques to eciently detect unobserv-
ability of mutations. An experimental evaluation of both techniques is planned
as future work.
