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...

Full description

Bibliographic Details
Main Authors: Aceto, Luca, Ingolfsdottir, Anna, Larsen, Kim Guldstrand, Srba, Jiri
Format: Book
Language:English
Published: Cambridge University Press 2007
Subjects:
Online Access:https://vbn.aau.dk/da/publications/bc659b00-a249-11dc-8188-000ea68e967b
Description
Summary: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.