Information Technology Reference
In-Depth Information
Examples for injected faults and mutations are provided in Section 3.5. The
common idea underlying both approaches is to make modifications to the system
and to run test cases that demonstrate the impact of these changes.
The following subsection provides a brief overview over the formal verification
techniques we apply to generate test suites from models containing mutations
or failure modes.
3.2
Bounded Model Checking
Model checking, in the most general sense, is a technique that explores the
reachable states of a model in order to determine whether a given specifica-
tion is satisfied [1]. It differs from testing in so far as it aims at an exhaustive
exploration of the state space of the model or program under test, thereby pro-
viding a correctness guarantee that is rarely achieved by means of testing. If
the specification is violated, model checking tools are often able to provide a
counterexample
, i.e., a witness that demonstrates how the specification can be
violated in the model.
Bounded model checking (BMC) is a variation of model checking which re-
stricts the exploration to execution traces up to a certain (user-defined) length
k
. BMC either provides a guarantee that the first
k
execution steps of the pro-
gram are correct with respect to the property
P
or a counterexample of length
at most
k
. The ability to report counterexamples is the essential feature we use
to generate test cases. The disadvantage of model checking is that it does not
scaleaswellastesting.
Figure 3a illustrates the schema of a Simulink model with a feedback loop.
Simulink diagrams comprise blocks instances and signals and wires represent-
ing the connections between these blocks. These components determine the in-
put and output signals (
i
and
o
, respectively) and the transition function
R
represented by the model. A bounded model checking algorithm unwinds such
models as indicated in Figure 3b; the signals
i
i
and
o
i
refer to the input and
output signals in the
i
th
step (or point in time), respectively, and
denotes an
undefined/non-deterministic signal value.
For the purpose of test case generation it suces to determine whether certain
states in a model are reachable. A model is specified by a formula representing
a (possibly partial) transition relation
R
(e.g., specified by means of a Simulink
diagram or ANSI-C program) and a predicate
I
that determines the valid ini-
tial states of the model. The transition relation
R
relates the current state of
the model to its successor states (i.e., the potential states after one step). The
structure of
R
may be further detailed by means of a
control flow graph
,which
partitions
R
into a separate transition function for each program location. This
simple formalism is suciently general to allow imperative models (such as C
programs or state charts) as well as data flow models (such as Simulink models).
Furthermore, the predicate
I
characterizes the set of valid initial states of the
model (this may be the safe or reset state of the system), i.e.,
I
(
s
)holdsif
s
is
a valid initial state.
