Modelling, Specification and Verification of Reactive Systems


Computing systems are everywhere in modern society. They are becoming increasingly sophisticated and they control key aspects of our lives. Think, for instance, of embedded computing devices, such as those that control ABS systems in cars, the temperature of our houses or the functioning of mobile phones. This population of 'effectively invisible' computers around us is embedded in the fabric of our homes, shops, vehicles, farms and some even in our bodies. They help us command, control, communicate, do business, travel and entertain ourselves, and these 'invisible' computers largely outnumber the desktop or laptop computers we see each day.

In light of the increasing complexity of such computing devices, and of the fact that they control important, when not altogether safety critical, operations, it is crucial to adopt high standards of quality in their development and validation. The key scientific challenge is to design and develop computing systems that do what they were designed to do, and do so reliably. In order to meet the challenge of building dependable systems, computer scientists are increasingly using model-based approaches to their design and validation. This means that, before actually constructing a system, one follows the time-honoured engineering approach of making a model of its design and of subjecting the model to a thorough analysis, whose ultimate aim is to certify that the design embodied by the model meets its intended specification.

The aim of this course is to introduce mathematical models for the formal description and analysis of programs, with emphasis on parallel, reactive and possibly real-time systems. The course deals with semantic models for parallel systems, languages for the description of their properties, and methods for showing that a model does afford some desired properties. As part and parcel of the course material, we also introduce automatic verification tools, and might hint at some of the implementation techniques underlying them. More specifically, after reviewing the fundamental model of Labelled Transition Systems, we will present a simple example of a process description language, namely, Milner's Calculus of Communicating Systems, its Structural Operational Semantics, the theory of bisimilarity and its connections with modal and temporal logics.

In a follow-up, three-session course, we will also briefly introduce timed automata, a key model for the description of real-time systems, their basic theory and a widely used tool for the verification of real-time systems described using networks of timed automata.