In February 1991, a Patriot missile defence system failed to track and neutralise a missile heading towards US Army barracks, resulting in death of 28 people. The report issued by the US General Accounting Office a year later blamed a software error. The growing dependence of our society on software that directly acts on the physical environment (including software in vehicles used for both civilian and military purposes) leads to the question: How do we make safety-critical software more reliable? In this post I discuss an approach to incremental construction of such software, based on a technique known as “refinement”.
Note, however, that the purpose of this post is not to develop a fully verified implementation of a system resembling Iron Dome; rather, my aim is to introduce the idea of refinement-based software system construction to those not familiar with formal approaches to software development.
Plethora of techniques available
Mature engineering disciplines rely on mathematics. Bringing mathematical reasoning into the process of software construction has been the focus of theoretical computer science at least since the 1960s. The research yield many techniques: from models of computations (finite state machines, Turing machines, lambda-calculus, Markov decision processes, process algebras), through logical languages for reasoning about such models (Hoare logic, type systems), to software implementations of tools based on these ideas (logical solvers, model checkers, theorem provers, program analyzers). Many variants of such tools and techniques exist: for deterministic, non-deterministic, stochastic, and adversarial systems; for non-timed, discrete-time, continuous-time and hybrid discrete-continuous systems; for pure and effectful computations, as well as for cyber-physical systems where computations interact with the physical reality.
The existence of this variety of techniques is good; however, it also poses an extra challenge to practicioners and researchers alike, as (1) different techniques are suitable in different situations, and (2) one can hardly be an expert in all of these. The problem is magnified by the fact that during a typical PhD work, one focuses on advancing the state-of-the-art of a small subfield of computer science, rather than on learning a bit about every technique present in the literature. Fortunately, these “formal” techniques of theoretical computer science are built on similar principles, so a person skilled in one can quickly adapt a different technique.
So which one?
For the Iron Dome exercise specifically, one has to look for techniques that allow proving safety guarantees (that is, the absence of “bad” outcomes) for hybrid discrete-continuous systems consisting of a physical “reality”, in the presence of adversarial non-determinism (e.g., we do not know when an adversaries’ rocket gets launched). One can also observe that the choice of implementation-level details (Which programming language? Microcontroller or FPGA?) is largely independent of the relatively simple specification (“no rocket explodes in the city, assuming all the rockets get fired from a point far enough and are slow enough”). The simplicity of the specification and complexity of possible implementation can be exploited by a refinement-based methodology: design decisions can be introduced gradually to a model of the system, until the model becomes detailed enough to be implemented. One technique suitable for such situation is Hybrid Event-B; another one would be Differential Refinement Logic. The rest of this post uses Hybrid Event-B in a somewhat informal manner; for a proper case-study, have a look at the Tackling the rugby club problem paper.
Models of Iron Dome
We will construct a series of models. A model as such is just a piece of code; the meaning of that piece of code is a collection of execution traces, each trace being a function from time (a non-negative real number) to a dictionary of named state variables. For all our Iron Dome models, one of such state variables would be the universe U of objects of our concern; another important variables would be pos_x,pos_y : U -> RR (where RR denotes the set of real numbers), representing the positions of all the tracked objects (that is, our geometric model would be only 2-dimensional). We would also have a variable color: U -> {red, blue}, specifying whether an object is an adversarial (red) or our own (blue), and a boolean variable alive : BB.
Variables change their values during events. One such event would be defensive action - any time a red object comes near (less than some constant ϵ) a blue object, all these objects near the blue one disappear, and the blue one disappears as well - that is, they are all removed from U (and from the domains of pos_x,pos_y,color). Another event would be hit, triggering whenever some red objects gets near to a point (say, a city) designated by constants x,y : RR – that is, nearer than some constant r (the radius of the city) in the x-axe and lower than some h in the y-axe – and setting alive to false. These events are instant (that is, they span zero time). The most abstract model (let’s call it M0) would also allow a continuous change of pos_x, pos_y in a continuous event of non-zero length. In any execution trace, instant and continuous events interleave.
In Hybrid Event-B, constants typically live in a so-called context. All our models share the same context, which could be written down as
CONTEXT C
SETS PU
CONSTANTS red, blue, ϵ, x, y, r
AXIOMS
x,y,r,ϵ ∈ RR
0 < ϵ,r,h, big_r
r < big_r
END
Here, PU is the superset of U containing all possible objects in our universe.
A simple model
Our “most abstract” model would be written down as (in a pseudo-syntax resembling the actual Hybrid Event-B)
MACHINE M0
TIME t
DISCRETE VARIABLES
U ⊆ PU
color : U -> { red, blue }
alive : BB
CONTINUOUS VARIABLES
pos_x,pos_y : U -> RR
EVENTS
evInit
STATUS discrete
WHEN t = 0
THEN
alive' = true
dom pos_x' = U
dom pos_y' = U
dom color' = U
∀ (u : U), x - big_r < pos_x' u < x + big_r
END
evDef
STATUS discrete
ANY ur,ub ∈ U
WHERE
color ur = red
color ub = blue
(pos_x ur - pos_x ub)**2 + (pos_y ur - pos_y ub)**2 ≤ ϵ**2
THEN
U' = { u ∈ U ∣ (pos_x u - pos_x ub)**2 + (pos_y u - pos_y ub)**2 > ϵ**2 }
pos_x' = restrict U' pos_x
pos_y' = restrict U' pos_y
color' = restrict U' color
alive' = alive
END
evHit
STATUS discrete
ANY ur ∈ U
WHERE
// color ur = red
alive = true
x - r < pos_x ur < x + r
pos_y ur < h
THEN
alive' = false
END
evMove
STATUS continuous
ANY v_x,v_y : U -> RR
SOLVE
D pos_x = v_x
D pos_y = v_y
END
END
Bodies of discrete events are predicates over primed and unprimed variables, where unprimed variables represent old values and primed variables new ones.
The initialization event evInit makes sure that all executions start in a “reasonable” state; the dom constructs returns the set of all inputs on which a function is defined (that is, the function’s domain). The defensive action event evDef removes some objects near some blue object b from U and updates the other variables accordingly. The continuous event evMove is parameterized by the velocities of the objects from U, and continuously updates the positions accordingly; the velocities can continuously change during the event.
A “safer” model – Refinement
One problem with the previous model is that a state with alive = false is reachable from some initial states. One reason for this is that evMove features non-deterministic parameters v_x, v_y, which are out of “our” control for both “red” and “blue” objects, and thus the environment can easily choose the velocities such that some red object hits the city. Now it would be the time to introduce a model that would give less capabilities to the adversary. Of course, the choice of such model depends on the kind of threat one wants to consider. However, we want to make sure that all new models behave “similarly enough” to M0, since M0 already captures the basic notions of our system. This “similar enough” relation is called “refinement”: we require that for every execution trace of a “new” model, there is a corresponding execution trace of the “old” model.
Note that our previous model already rules out teleportation; hence, we could try to refine it to a safer model (that is, a model where alive = false is unreachable in all execution traces) by (1) requring that blue objects do not move at all (their velocities in evMove are zero), and (2) requring that the system starts with an initial state where there are enough blue objects surrounding the city.
MACHINE M1
REFINES M0
...
evInit
STATUS discrete
WHEN t = 0
THEN
...
∃ (rr : RR), r < rr < big_r /\ ∀ (px py : RR), |px - x| = rr -> ∃ (bu : U), color' bu = blue /\ pos_x' bu = px /\ pos_y' bu = py
END
evMove
STATUS continuous
ANY v_x,v_y : U -> RR
WHERE ∀ (bu : U), color bu = blue -> (v_x bu) = 0 /\ (v_y bu) = 0
SOLVE
D pos_x = v_x
D pos_y = v_y
END
...
Well, maybe having two continously dense columns of blue objects is a bit unrealistic. And since explosions of blue objects would destroy blue objects as well, this would protect only against one red object. So this example serves only as an illustration of what a refinement is. (We skip all the proofs in this post.)
A more realistic model
In a more realistic model, objects would have velocities that could get changed when applying forces to the objects. We can also ‘bake in’ an assumption that there is no force applied to red object - as would be the case of unguided missiles in the absence of gravity.
MACHINE Munguided
REFINES M0
...
CONTINUOUS VARIABLES
pos_x,pos_y : U -> RR
v_x,v_y : U -> RR
mass : U -> RR
...
evInit
...
∀ u, mass u > 0
END
evMove
STATUS continuous
ANY f_x, f_y : U -> RR
WHERE ∀ (ru : U), color ru = red -> f_x ru = 0 /\ f_y ru = 0
SOLVE
D v_x = f_x / mass
D v_y = f_y / mass
D pos_x = v_x
D pos_y = v_y
END
END
(We slightly abuse the notation and use the division operator (’/’) to denote point-wise division of functions.)
The intuitive argument why Munguided refines M0 would be: (1) there are more variables in Munguided than in M0, and thus we can project traces of Munguided back to (would-be) execution traces of M0; (2) evInit is only stricter in Munguided than in M0, thus only possibly filtering out some execution traces; and (3) each evMove in Munguided can be simulated by an evMove in M0.
But.. why?
But is this useful at all? Why going through the hassle of creating and maintaining such models? There are several reasons.
Make assumptions explicit
First, if we ever establish any property about a model, be it through a simulation or through a formal proof, it would be established from the assumptions encoded in the model. This is especially useful when doing proofs: the process of proving something forcese us to write down the assumption needed for the proof, and thus it becomes much clearer what is our defense and threat model.
Refine down to code
Second, the refinement process can be used to derive an algorithmic code. One necessary step for doing so would be discretization of continuous event when doing refinement; this is well-supported in Hybrid Event-B (and I may want to write another post about that).
Communicate
Third, one can send such models and proofs about them to colleagues. Since such models have a precise meaning, the risk of a message being lost in the noise in human communication is much lower than when communicating through a natural language, or through drawings.
Conclusion
Hybrid Event-B was designed by Richard Banach, so if it caught your interest, feel free to check his papers.