Jan Friso Groote and Mohammad Reza Mousavi: Modeling and Analysis of Communicating Systems
MIT Press, 2014, ISBN 978-0-262-02771-7,
The book Modeling and Analysis of Communicating Systems by Jan Friso Groote and Mohammad Reza Mousavi introduces the foundations for modeling concurrent systems as transition systems, the key notions of equivalence and of bi-simulation between transition systems, and their use in the specification and verification system mCRL2. Though rooted in the mCRL2 technique, the book presents general principles that should be of interest not only for readers who want to learn about mCRL2, but also for readers interested in general in modeling and verification of complex systems.
This review is written by Matteo Rossi for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community. The review has also appeared in Formal Aspects of Computing (link).
Modeling and Analysis of Communicating Systems
by Jan Friso Groote and Mohammad Reza Mousavi
To begin, the book provides foundations for modeling concurrent systems as transition systems and introduces the key notions of equivalence and of bi-simulation between transition systems. Those notions are used throughout the book to define the intended correspondence between the desired and the actual behavior of the system being analyzed. The book also presents higher-level notations to define transition systems as communicating processes and to express properties of interest in terms of the μ-calculus. It also introduces various techniques for proving properties (e.g., to establish a bi-simulation between abstract and concrete behaviors) in the presented setting. Examples of proofs carried out using the aforementioned techniques are provided throughout the book, and the results of some extensive case studies are presented. These case studies show the considerable depth and precision that can be achieved using the authors' approach. The formalism introduced is based on a powerful set of types that allow one to express not only the interactions among communicating processes, but also the information exchanged with a notable level of detail. Chapter 8 deals with the modeling of real-time systems, but, for the most part, the focus is on models where time is purely qualitative.
The book should be accessible to anyone interested in the precise mathematical modeling of concurrent systems. It could be used as textbook for a course at the master or PhD level focusing on the dual issues of formally modeling and proving properties of complex systems. To avoid overwhelming the reader with mathematical details, the book describes the hardcore details of the semantics of the introduced concepts in the last (optional) chapter. However, the book is not—nor one can expect it to be given the topic treated—an easy read. A prerequisite for prospective readers is expertise and a deep interest in mathematical modeling.
The book emphasizes techniques useful for proving the correspondence between concrete and abstract behaviors. Indeed, the ability to prove deep properties of modeled systems and, while doing so, of considering rich, general data types (not restricted to, say, finite domains) is a strength—indeed, in the reviewer’s opinion, the key strength—of the presented approach. In this sense, the focus on proofs that, while tool-supported, still require significant ingenuity from those analyzing the models differentiates this book from recent literature (see, e.g, [BK08,KS16,CHVB18]), which in large part focuses on fully automated formal verification of modeled systems and requires significant simplification and abstraction to achieve automatic verification. Although fully automated formal verification can be valuable, the various examples of proofs presented throughout the book, many of them non trivial, demonstrate how the authors' approach provides deep insights into the intricacies of the modeled systems and how the approach guarantees the correctness of the designed processes. The historical notes of Chapter 14 show how formal proofs can provide a level of assurance that years of practice and of testing have difficulty achieving. However, while the benefits of the author’s approach are significant, the level of expertise necessary to carry out formal proofs in practice is considerable.
In summary, the book should be of interest to many prospective readers, though it is probably not for all tastes. The book clearly shows the power of formal models and of formal proofs but does not hide the complexity and difficulty of formal modeling and formal verification.
[BK08] Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.
[CHVB18] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018.
[KS16] Daniel Kroening and Ofer Strichman. Decision Procedures. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2016.