Reactive Systems: Modelling, Specification and Verification

A reactive system comprises networks of computing components, achieving their goals through interaction among themselves and their environment. Thus even relatively small systems may exhibit unexpectedly complex behaviours. As moreover reactive systems are often used in safety critical systems, the need for mathematically based formal methodology is increasingly important. There are many books that look at particular methodologies for such systems. This book offers a more balanced introduction for graduate students and describes the various approaches, their strengths and weaknesses, and when they are best used. Milner's CCS and its operational semantics are introduced, together with the notions of behavioural equivalences based on bisimulation techniques and with recursive extensions of Hennessy-Milner logic. In the second part of the book, the presented theories are extended to take timing issues into account. The book has arisen from various courses taught in Denmark and Iceland and is designed to give students a broad introduction to the area, with exercises throughout.