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