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.