This sample shows how to do safety analysis in PyModel: write invariants (safety conditions) that describe safe states, then use exploration to search for unsafe states. Unsafe states are indicated in the printed output from pma (or pmv), and in the generated FSM and graphics files.

The example here is a microwave oven. The safety condition is: the microwave power can only be on when the oven door is closed.

• unsafe_oven: model program for an unsafe oven. The enabling conditions and action bodies allow traces that can reach an unsafe state.

• oven: model program for a safe oven. The enabling conditions and action bodies ensure that traces can only reach safe states.

• test_graphics: generates FSMs and graphs from both models. When you run this script, the pma program prints the number of unsafe states found in each model.

• fsmpy, svg: directories of output files from test_graphics. The unsafe states are indicated in these output files.

Examine the generated FSM files (in the fsmpy directory). They are Python modules (in plain text).

• unsafe_ovenFSM.py: FSM generated from unsafe_oven. The comments at the top indicate 1 unsafe states. Further down, the states dictionary reports each state, along with its state variables and their values. Below that, unsafe is a list of unsafe states, identified by their keys in states: unsafe = [3] here.

• ovenFSM.py: FSM generated from oven. The comments at the top indicate 0 unsafe states and the unsafe list is empty.

View the generated graphics files (in the svg directory) in a browser. Hover the pointer over any state bubble to see a tooltip that shows the state variables and their values in that state, to confirm whether the safety condition is satisfied. Unsafe states are colored red.

• unsafe_ovenFSM.svg: graph of unsafe_oven. The unsafe state appears in red.

• ovenFSM.svg: graph of oven, confirms there are no unsafe states.

There is no stepper in this sample.

Revised Apr 2013