CS7052: The Specification and Analysis of Reactive Systems
This is a one semester course, given in Hilary term 2013-14, introducing students to the theory and practice of Reactive Systems.
The course is based on the book
Reactive Systems: Modelling, Specification and Verification
by Luca Aceto, Anna Ingolfsdottir, Kim Larsen and Jiri Srba.
Cambridge University Press, 2007.
Prerequisites: Basic discrete mathematics, including elementary set theory, propositional logic and induction.
Objectives: To introduce students to the mathematical theory underlying formal reasoning techniques for distributed and concurrent systems.
Learning outcomes: On completion of the course students will be able to:
- use a process calculus such as CCS to describe the behaviour of systems at different levels of abstraction
- describe computational properites of systems using modal and temporal logics
- understand the basic principles underlying the behavioural equivalence of systems
- use verification tools to compare descriptions of system behaviour and to determine their properties.
Coursework: This is based on weekly tutorials in which the concepts and techniques will be applied to simple example systems. Students will also be expected to treat these examples using some automatic verification tools.
References: The course textbook is:
Reactive Systems: Modelling, Specification and Verification,
by Luca Aceto, Anna Ingolfsdottir, Kim Larsen and Jiri Srba.
Cambridge University Press, 2007.
