Reactis
Lustre
stateflo w Simulink Gateway
safe state
machines
nusmV
Prover
AcL2
sAL symbolic
model checker
Rockwell collins/u of minnesota
esterel technologies
sRi international
Reactive systems
mathWorks
sAL
sAL Bonded
model checker
sAL infinite
model checker
based on the counterexamples. Since
many model checkers already implement this technique, we have not tried
to incorporate it into our translator
framework.
We have developed tools to translate
the counterexamples produced by the
model checkers into two formats. The
first is a simple spreadsheet that shows
the inputs and outputs of the model for
each step (similar to steps noted in the
accompanying table). The second is a
test script that can be read by the Reactis tool to step forward and backward
through the counterexample in the
Reactis simulator.
Our translator framework currently
supports input models written in Simulink, Stateflow, and SCADE. It generates specifications for the NuSMV, SAL,
and Prover model checkers, the PVS
and ACL2 theorem provers, and C and
Ada source code.
troller enters the Suspended submode.
From the Suspended submode, the operator can return to Cooking submode
by pressing the Start button while the
door is closed, or return to Setup mode
by pressing the Clear button. When
Steps Remaining decrements to zero,
the controller exits Running mode and
returns to Setup mode.
Since this model consists only of
Boolean values (Start, Clear, Door
Closed), enumerated types (mode),
and two small integers (Steps Remaining and Steps to Cook range from 0 to
639, the largest value that can be entered on the keypad) it is well suited
for analysis with a symbolic model
checker such as NuSMV. A valuable
property to check is that the door is
always closed when the microwave is
cooking. In CTL1 (one of the property
specification languages of NuSMV),
this is written as:
AG(Cooking -> Door _ Closed)
A small example
To make these ideas concrete, we pres-
ent a very small example, the mode log-
ic for a simple microwave oven shown
in Figure 2. The microwave initially
starts in Setup mode. It transitions to
Running mode when the Start button
is pressed and the Steps Remaining to
cook (initially provided by the keypad
entry subsystem) is greater than zero.
On transition to Running mode, the
controller enters either the Cooking or
Suspended submode, depending on
whether Door Closed is true. In Cooking
mode, the controller decrements Steps
Remaining on each step. If the door is
opened in Cooking mode or the opera-
tor presses the Clear button, the con-
Translation of the model into
NuSMV and checking this property
takes only a few seconds and yields the
counterexample shown in Table 1.
figure 2. microwave mode logic.
rUnnInG
SeTUP
entry: mode = 1;
{steps_remaining
= steps_to_cook;}
[start &&
steps_remaining > 0]
[steps_remaining > 0]
/steps_remaining- -;
COOKInG
entry: mode = 2;
1
[steps_remaining <= 0]
2
1
[door_closed]
[clear]
2
[start && . . .
door_closed]
SUSPended
entry: mode = 3;
2
[clear || . . .
!door_closed]
1