Reactive Systems: Modelling, Specification and Verification
Introduction
“Formal methods is a term used to describe the specification and verification of software systems and software using mathematical logic. There are many books that look at particular methodologies for such systems, for example, this book offers a more balanced introduction for graduate students that describes the various approaches, their strengths and weaknesses, and when they are best used. This book emerged from a variety of courses taught in Iceland and Denmark and is designed to give students a broad introduction to the area, with exercises throughout.” Welcome to the homepage for the book “Reactive Systems: Modelling, Specification and Verification”. The book has been used for courses on modelling and verification of reactive systems at several universities (here is a list of some of them). If you are using the book for one of your courses, please send us an email with the name of the course, its level and a URL pointing to the web-page for the course. We would like to keep track of our “user group”. Thank you.
Recommendations
Many modern day computing systems are reactive in nature; they persist indefinitely, responding to the interactions of users, and updating their internal structures accordingly. Over the last two decades an elegant theory of these reactive systems has emerged, and is being increasingly applied in industrial settings. And at last we have an accessible text book for this area, written by a team who have played a central role in the development of the underlying theory, and the software tools which are essential to its successful application. It treats both timed and untimed systems, and although the underlying theory is carefully and methodically explained, the main trust of the book is to engage students with the material via a wealth of thought-provoking examples. The clarity of the exposition is exceptional; it presents the essential ideas clearly, avoiding unnecessary detail, but at the same time has well-chosen pointers to more advanced concepts. The book is destined to become the standard textbook for reactive systems. Prof. Matthew Hennessy, University of Sussex, UK A must for anybody interested in formal analysis techniques for computing systems. Prof. Wan Fokkink, Vrije Universiteit Amsterdam , The Netherlands This book offers an introduction to model-based verification of reactiveu0026hellip;
Course Material
We provide here different resources for teacher’s using our book.
Lectures/Slides
Examples of our lectures using this book are here: Modelling and Verification 2009 – Reykjavík University – Three-week intensive course Semantics and Verification 2008 – Aalborg University Modelling and Verification 2006 – Reykjavík University Semantics and Verification 2004 – University of Iceland A package with latex slides (including latex sources) used by Jiri Srba in 2005-2007 at Aalborg University in Denmark can be downloaded here. Please, read the file README.txt for further information regarding the use of the slides and the compilation of the files. A package with latex slides (including latex sources) with some pictures of timed automata and TLTSs from Part II of the book can be downloaded here. Here are examples of courses from other universities that use our book: Introduction to Concurrency and Verification – University of Salzburg Modelling and Verification – Technical University of Ostrava Dependable Systems and Software: Nebenläufige Programmierung – Universitäet Des Saarlandes (See here for the full reading list for this course.) Semantics (Q1,’07) – University of Aarhus Software Specification – Technical University Eindhoven Metodi Formali per la Concorrenza – Università di Padova Analyse des Programmes et Sémantique – Master d’Informatique UPMC — M1 STL — 2007/2008 APS Real Time Systemsu0026hellip;
Exercise Solutions
Solutions to selected exercises can be forwarded to the lecturers using our book. Please, contact us if you want to receive a solution list and please include the link to your course homepage and your role in the course. Thank you.
Project Ideas
Further Exercises and Project Ideas Using Uppaal. A list with 27 suggested exercises is available here. The book “The little book of semaphores” by Allen B. Downey presents semaphore-based solutions to many concurrency problems, ranging from classical ones (like the barbershop) to tricky and obscure problems (like the Sushi bar). All of these problems are a suitable source of student projects on modelling and verification using Uppaal. (The pointer to Downey’s book is courtesy of Frits Vaandrager.) Using Uppaal (or the Concurrency Workbench, if you prefer) model the mutual exclusion algorithm proposed by Murray A. Eisenbeng and Michael R. McGuire (“Further comments on Dijkstra’s concurrent programming control problem”, Communications of the ACM 15(11):999 (November 1972)) for three processes, and establish that the algorithm does guarantee mutual exclusion. The code for process i is given below. do { // Acquire lock while(1) { flag[i] = WantIn; j = turn; while (j != i) { if (flag[j] != idle) j = turn; else j = (j + 1) % n; } flag[i] = InCS; j = 0; while ((j u003c n) u0026#038;u0026#038; (j == i || flag[j] != InCS)) j++; if ((j u003e= n) u0026#038;u0026#038; (turn == i || flag[turn] == Idle)) break; // Acquiredu0026hellip;
Additional Reading
Here we shall present pointers to other related reading material, interesting links, etc. Feel free to suggest further additions by writing to us! Supplementary Text for the Book Additional Remarks on the Linking Combinator. This short note explains the role played by the relabelling in the definition of the linking combinator used in Exercise 2.13 on page 30 of the book. Some Remarks on Time Additivity in Timed Labelled Transition Systems. This short note discusses some variations on the axioms for timed labelled transition systems, as defined on pages 164-165 of the book. SOS Meta-theory: A Very Short Introduction. This note discusses some possible generalizations of the congruence theorem for bisimilarity over CCS presented in Theorem 3.2, pages 46-49 of the book. It uses this topic to offer a very short introduction to the meta-theory of structural operational semantics. Deciding Bisimilarity over Finite Labelled Transition Systems is P-complete. This note discusses a proof of a result by José L. Balcázar, Joaquim Gabarró and Miklos Santha to the effect that checking various forms of bisimilarity introduced in the book is P-complete. Papers in Concurrency Theory A Brief History of Process Algebra by Jos Baeten. Computing with actions and communications by Wanu0026hellip;
Tools
The Edinburgh Concurrency Workbench UPPAAL The Bisimulation Game Game (including the CCS visualizer and simulator) Concurrency Workbench of the New Century mCRL2 CADP CCS in Maude. Thanks to Mikito Iwamasa (System Engineering Laboratory, Corporate Ru0026#038;D Center, Toshiba Corp.) for pointing out this link. CCS+HML in Haskell courtesy of Arnar Birgisson IBEN (for readers who want to play with Binary Decision Diagrams)
Errata
Here are the errata.
Contact
To contact the authors of this book, send an email to rsbook (at) cs.aau.dk.
Errata
Errata list
updated on September 9th, 2014.