Solutions to In-Class Exercises

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);
    }

    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.