Programming Logic for Complex Systems This course covers program verification methods for a class of programs, commonly referred to as reactive programs. Reactive programs typically never terminate and are run in order to maintain some interaction with the environment. An adequate description of reactive systems must refer not only to initial and final states, but also to the ongoing behaviour as a (possibly infinite) sequence of states and events. The purpose of this course is to investigate the use of logical calculi for the specification, design and verification of reactive systems. Topics include: modelling of discrete event systems, semantics of real-time languages, logical and discrete calculi (e.g. temporal logic) for specifying and verifying safety, liveness, deadlock, priority and fairness properties of reactive programs, and prolog tools for automating verification

Safety critical systems are complex systems that interact with a dangerous environment 9e.g. nuclear reactors or radiation therapy machines for treating patients with cancer). 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.

As explained by J.R. Abrial in his new book on Event-B, these methods and tools will provide insights on modelling and formal reasoning for such systems. These activities are supposed to be performed before undertaking the effective coding of a computer system, so that the system in question will be correct by construction. The methods will include the ability to develop sequential programs, concurrent programs, distributed programs, electronic circuits, reactive systems, etc. We will construct a mathematical model of a program that is quite different from the program itself. And we will learn that 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 sometimes long sequence consisting of gradually building more and more accurate models of the future program (think of the various blue-prints made by an architect).

Winter 2009:

Mondays and Wednesdays: 11:30am-1pm R N836