Information Technology Reference
In-Depth Information
o
i
R
(a) Schema of a Simulink model with a loop
o 0
o 1
i 0
i 1
R
R
l 1
(b) Unwinding of the model in Figure 3a
Fig. 3. Unwinding Simulink models
A path (or execution trace) π of the model is a sequence of states s 0 ,s 1 , ..., s n
such that the adjacent pairs s i ,s i +1 of states in that sequence are related by R
(i.e., n− 1
i =0 R ( s i ,s i +1 )), and I ( s 0 ) holds (i.e., s 0 is a valid initial state). A state
is induced by the values of the variables (or wires and signals) of the model. In
reactive models, the variables are typically partitioned into input variables, hidden
(or internal) variables, and output variables. The observable part of an execution
trace is therefore the sequence of inputs and the resulting sequence of outputs.
Given a state s i ,weuse s i .i to refer to the input, and s i .o to denote the output.
3.3 Equivalence Checking
Formal Equivalence Checking is a technique used to formally prove that two
models M and M exhibit the same observable behavior [19]. This is achieved by
comparing the input and the output behavior of the two models. To construct a
test-scenario (i.e., a sequence of input/output pairs), we are interested in checking
whether for a given input sequence the outputs in the first k steps of the execu-
tions of the models match. This notion of “ k -equivalence” is decidable, assuming
that the input and output values have a finite range.
Whether two given models are k -equivalent can be decided using model check-
ing. Given two models M and M (comprising the transition functions R and R
and the initial state predicates I and I , respectively), we can check (assuming
that the size of the states is finite) whether the following is satisfiable:
k
k− 1
s i .i = s i .i
equality of all inputs
I ( s 0 )
R ( s i ,s i +1 )
i =0
i =0
first model
(1)
k− 1
k
I ( s 0 )
R ( s i ,s i +1 )
= s i .o
inequality of an output
s i .o
i =0
i =0
second model
Search WWH ::




Custom Search