This lecture and problem set were given after this reading assignment about safety-critical systems, which discusses the linear accelerator example.

You can view software development from two sides: the inside or the outside. The inside view considers how the product is built and how it works. The outside view considers how the product is used and its consequences in the world. It is important to consider both.

The purpose of this assignment is to give you a taste of one way to think about the outside view: consider the states the system (not just the program) is allowed to be in and propose transitions that get the system from one state to another. Make sure the state transitions provide a way to get to the intended goal state, while ensuring that they cannot enter any forbidden states. These are the central ideas in many formal analysis methods.

A *state* is a "state of affairs", the important properties of
the system at one point in time. The state can be represented by a
collection of *variables* and their *values*. The
allowed states can be represented as restrictions on the values of the
variables, and behavior can be represented by changes in the values
of the variables.

We need to represent the variables (etc.) in some convenient notation that has a clear meaning. In this exercise we will use fragments of the C programming language (which is similar to Java, Perl, and other popular languages). However, we are not writing a program here. Instead, we are using the notation to model and analyze a system. We're modelling the whole system, so the variables need not be variables in a computer program. They can represent quantities or situations in the world outside the computer. Moreover, we're modelling the system at an abstract level so we can leave out a lot of the details you would have to put in to make a program work.

An example should help make this clear. Consider an electron linear accelerator with two modes. When the operator selects electron mode, the beam current is set low and the target is moved out. When the operator selects X-ray mode, the beam current is set high and the target is moved in. The operator can turn the beam on, and the beam turns off when various events occur. This system can be represented by three state variables. In C they can be declared like this:

enum current_t { low, high } current; enum target_t { in, out } target; enum beam_t { off, on } beam;

The first declaration declares a variable named `current`

that
can take on the values `low`

and `high`

(`current_t`

is not the variable, it is required by C syntax
but we can ignore it).

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

We can describe a state by writing a boolean function that returns true when the system is in that state (we can use the name of the function as the name of the state). For example this function describes the state where the beam is on in electron mode: the current is low, the target is out, and the beam is on:

boolean electron_beam(void) { return (current == low && target == out && beam == on); }

Here `==`

is the equality operator and `&&`

is
the logical *and* operator. Don't worry about
`void`

, C syntax requires it.

A state function is a boolean function whose return value depends only on state variables. The preceding state function describes just one state but we can also describe sets of states.

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

**Exercise:** Write the `xray_mode`

state function.

Remember we are using these functions to name and describe states for purposes of modelling and analysis. We're not going to write any main program that calls these functions.

We represent dynamics by writing *state transitions* where the
values of variables change. We model state transitions (and give them
names) by writing C functions. This function describes the transition
where the operator selects electron mode:

void select_electron_mode(void) { if (beam == off) { current = low; target = out; } }

Each state transition has this form. First there is an
`if`

statement that tests a boolean expression on the
system state called the *guard*. If the guard is true, the
system executes the body of the `if`

, which is always a
sequence of assignments that change the values of some of the state
variables. After the transition completes, those variables have their
new values and the values of any other variables remain unchanged. If
the guard is false, the values of all the variables remain unchanged
(no transition occurs).

We're not going to write any main program that calls the transition
functions. Instead we're going to assume the system behaves as
follows. A transition whose guard is true is *enabled*. If a
transition is enabled, the system executes it. Several transitions
may be enabled at the same time; in that case the next transition is
selected *nondeterministically* (at random). Each transition
is *atomic*: once begun, it runs to completion without
interruption -- there are no "in-between" states.

It turns out that this simple scheme is quite expressive and can model many interesting systems, including most computations. Note that all the control structure is encoded in the guards.

**Exercise:** Write the `select_xray_mode`

transition.

An essential task in the design of any safety-critical system is to
identify the safe states. A system is safe if it is always in a safe
state (it never enters an unsafe state). Safe states can be
represented by state functions. A state function that is intended to
return true in every state that the system can reach is called an
*invariant* (its truth never varies). Safety requirements can
be represented by invariants. A system which is always in a safe
state is said to satisfy its safety invariant. A system which can
reach a state where the safety invariant is false is said to violate
the invariant --- it can enter an unsafe state.

The electron accelerator is unsafe if the beam is on while the current is high but the target is out, because in this state the dose rate is much too large.

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

. You may use the
`electron_mode`

and `xray_mode`

state functions
defined previously. Hint: use the logical *or* operator `||`

to combine separate cases.

To perform a safety analysis, check whether it is possible for the system to violate its safety invariant. To do this you must know the initial state, all the transitions, and the safety invariant.

We add these transitions to our system:

void beam_on(void) { if (beam == off) beam = on; } void beam_off(void) { if (beam == on) beam = off; }

Assume the system starts up in the `electron_mode`

state
with `beam = off`

.

**Exercise:** Does this system satisfy its safety invariant? Why?

We add these transitions to our system:

void target_in { if (beam == off) target = in; } void target_out { if (beam == off) target = out; }

**Exercise:** Does the system satisfy the invariant now? Why?

Imagine a program the could do the safety analysis automatically. Given a set of transitions, a safety invariant, and an initial state, the program reports whether the invariant can be violated, and if so, it shows how.

**Exercise:** Would this be possible for our example? Is it
possible in general?

Let's extend the model to make it a bit more realistic. We'll add a dosimetry system. The accelerator operator can enter a preset dose. The accelerator control system monitors the dose that accumulates while the beam is on. The accumulated dose must not exceed the preset dose, except for a small tolerance. When the beam is on and the accumulated dose reaches the preset dose, the beam turns off (the beam may still turn off for other reasons before the preset dose is reached). The operator can reset the accumulated dose back to zero when the beam is off. For simplicity we'll assume the preset and accumulated doses are always whole numbers (integers) whose values are zero or greater, and the tolerance is a small positive integer greater than zero. We can declare the new state variables this way (where /* ... */ delimits a comment).

int dose; /* accumulated dose */ int preset; /* preset dose */ int tol; /* small constant tolerance by which dose may exceed preset */

Write up and hand in your solution to the following homework exercises. Don't worry about programming language syntax. You may write your solutions in some language other than C or even in pseudocode if you prefer.

**Exercise 1:** Write the safety invariant `safe_dose`

to express that the accumulated dose must not exceed the preset dose,
except for a small tolerance.

**Exercise 2:** Write the system safety invariant
`safe_accelerator`

that expresses all the safety
requirements in both `safe_mode`

and
`safe_dose`

.

**Exercise 3:** Write the state transition `beam_off_dosim`

to express that the beam turns off when the accumulated dose reaches or
exceeds the preset dose.

**Exercise 4:** Write the state transition `deliver_dose`

to express that the accumulated dose increases by the constant
amount `delta`

during each unit of time that the beam is
on (where a time unit is the smallest interval that the system can resolve).
**Hint:** This is easy. You do not need any new variables,
other than `delta`

. Note that this transition will usually
occur many times each time the beam is on.

**Exercise 5:** Consider the system comprising all the items
defined previously, except the potentially unsafe transitions
`target_in`

and `target_out`

are not included.
The system is initialized in `electron_mode`

with
`beam = off`

and `preset`

and `dose`

initialized to any values that satisfy `safe_dose`

. Does
this system satisfy the system safety invariant? If not, describe
what can go wrong, using the variable names and other terminology of
the model.

Something to think about (not to hand in): Exercise 4
describes a constant dose rate. It would be more realistic to
say the prescribed dose increases by *at most* `delta`

during each time unit. Can we express this in our programming language
notation? If not, how could the notation be extended?

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 (also here), Spin, and Alloy again.

Jonathan Jacky,