Here are my solutions to the in-class exercises posed in the handout, State-based safety analysis.

**Exercise:** Why did we not include another state variable to
represent the mode (X-ray or electron)?

Because it would be redundant. The three state variables we already have provide sufficient information to determine the mode. Moreover, there are states don't belong to either mode, so if we had a mode variable we would need one (or more) values to indicate that. But this was a judgment call - sometimes it is thought to be useful to include redundant variables as a kind of documentation.

**Exercise:** Here is another state function for this system. How
many distinct states does it describe? What are they?

boolean electron_mode(void) { return (current == low && target == out); }

It describes two distinct states, where the variables *not*
mentioned in the state function take on all possible values:

current == low && target == out && beam == off current == low && target == out && beam == on

**Exercise:** Write the `xray_mode`

state function.

boolean xray_mode(void) { return (current == high && target == in); }

`select_xray_mode`

transition.
void select_xray_mode(void) { if (beam == off) { current = high; target = in; } }

Note that after `select_xray_mode`

occurs, `xray_mode`

is true.

**Exercise:** Write the safety invariant
`safe_mode`

.

The natural language requirements say, "The electron accelerator is unsafe if the beam is on while the current is high but the target is out." Translating this to a boolean expression, we get:

beam == on && current == high && target == out

That's the unsafe state. To get the safe states, we negate this and apply DeMorgan's law:

boolean safe_mode(void) { return (beam == off || current == low || target == in); }

This answer includes all the safe states. If you use intuition and
the modes defined previously, you might propose ```
beam == off ||
electron_mode || xray_mode
```

. This is not quite the same because
it excludes the useless but safe state ```
beam == on && current ==
low && target == in
```

. Just ```
electron_mode ||
xray_mode
```

is simplest but it excludes even more states.
All three answers are reasonable, however.

**Exercise:** (After we add the `beam_on`

and
`beam_off`

transitions) Does this system satisfy its safety
invariant? Why?

Yes, because every transition we have defined leaves the system
in `electron_mode`

or `xray_mode`

, which
are in both `safe_mode`

.

**Exercise:** (After we add `target_in`

and
`target_out`

) Does the system satisfy the invariant now?
Why?

No, because `target_out`

can occur when ```
beam_off &&
xray_mode
```

, then `beam_on`

can occur. That results
in the unsafe state ```
beam == on && current == high && target ==
out
```

.

**Exercise:** (Regarding automatic analysis) Would this be possible
for our example? Is it possible in general?

It would be possible for our example because there are few enough states and transitions that a program can examine all possible transitions from all possible states. But if the number of states and transitions is large, this is not feasible.

We ran out of time so I didn't have time to explain that there are whole technologies devoted to writing and analyzing models like this. They are examples of formal methods. They include the modelling notations Alloy, ASM, TLA, Unity, VDM, and Z (also here), the theorem provers ACL2, PVS, and Z/EVES, and the model-checkers SMV, Spin, and Alloy again.

Jonathan Jacky,