Safety critical systems are complex systems that interact with a dangerous environment (e.g. nuclear reactors, medical devices such as radiation therapy machines such as the Therac-25 for treating cancer patients, and airplanes). The specification and design of software and hardware for such systems is challenging because these systems may result in death or serious injury to people, loss or severe damage to equipment or environmental harm. So ordinary testing methods are insufficient to ensure that they work reliably and safely.

In this course, we use industrial strength methods and tools such as Event-B, Alloy and Spin for the design of safety critical systems. These methods and tools are all in use in actual practice in industry.

As explained by J.R. Abrial in his new book on Event-B, these methods and tools provide insights into specifying, modelling, and reasoning about the safety and correctness of such systems. These activities take place before undertaking effective coding of a computer system, so that the system in question will be correct by construction. The methods we will look at include the ability to develop sequential programs, concurrent programs, distributed programs, electronic circuits, reactive systems, etc.

We construct a mathematical model of a program that is quite different from the program itself. It is far easier to reason about the model than about the program. We will study important notions such as abstraction and refinement: the idea being that an executable program is only obtained at the final stage of a sequence consisting of gradually building more and more accurate models of the future program (think of the various blue-prints made by an architects and engineers).

“Professional engineers can often be distinguished from other designers by the engineers’ ability to use mathematical models to describe and analyze their products.” (David L. Parnas, “Predicate Logic for Software Engineering”).