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 reactive systems, a technology which is essential to all IT-developers of the future, given the global trend in information technology towards ubiquitous computing.
The book is unique in its pedagogical style, introducing the required theory (of models and specification formalisms for reactive systems) motivated carefully with its applications (in the development and use of automated verification tools in practice), and written as a textbook which can be used readily at many different levels of IT-related curricula.
Prof. Mogens Nielsen, Aarhus University, Denmark
This book is a gentle introduction to the basics of theories of interactive systems that starts with an introduction to CCS and its semantic theory and then moves to introducing modal logics and timed models of concurrency. By means of a number of small but intriguing examples and by using software tools based on sound theoretical principles, it leads the reader to appreciating and mastering a number of process algebra based techniques that are having a great impact also outside academic circles.
The authors have managed to concentrate their expertise, enthusiasm and pedagogical ability in less than 300 pages. The presentation is very clear and conveys sufficient intuition to make the book adequate also for students with limited mathematical background. An excellent advanced undergraduate text.
Prof. Rocco De Nicola, Universita’ di Firenze, Italy