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.
RecommendationsMany 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 MaterialWe provide here different resources for teacher’s using our book.
ToolsThe 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)
ErrataHere are the errata.
ContactTo contact the authors of this book, send an email to rsbook (at) cs.aau.dk.

Course Material

Here we provide different resources for teacher’s using our book:

Giving lectures using our book, links, slides.
Solutions to selected exercises.
Ideas for projects.
Supplementary reading material.

Reactive Systems: Modelling, Specification and Verification

Proudly powered by WordPress