Groote and Mousavi introduce the theoretical foundation of the modeling and analysis language mCRL2. mCRL2, along with its extensive toolset, is available online (http://www.mcrl2.org). Though the program is available on Windows platforms, the authors recommend Mac OS or Linux platforms for better interfaces.

The following is a good summary of the book that appears on the back cover:

Complex communicating computer systems--computers connected by data networks and in constant communication with their environments--do not always behave as expected. This book introduces behavioral modeling, a rigorous approach to behavioral specification and verification of concurrent and distributed systems. It is among the very few techniques capable of modeling systems interaction at a level of abstraction sufficient for the interaction to be understood and analyzed.

The book is divided into four major parts. Part 1, “Modeling,” has eight chapters. The mathematical foundation that underpins various concepts, such as calculus of computing systems (CCS), algebra of communicating processes (ACP), and communicating sequential processes (CSP), are discussed. Data abstractions and data types, which are important aspect of mCRL2, are addressed in chapters 2 and 3. The sequential and parallel processes are discussed in chapters 4 and 5. The modal μ-calculus is discussed in chapter 6. Examples of system behavior modeling, such as a patient support platform, are addressed in chapter 7. Systems with timed process behavior, including time-critical processes, are discussed in chapter 8.

Part 2, “Analysis,” has six chapters that deal with the analysis, manipulation, and verification of the processes being modeled by mCRL2. Chapters 9 and 10 introduce the transformation and manipulation of processes; various techniques are discussed, including the recursive specification principle and linear form transformation. Chapters 11 and 12 deal with the transformation of processes based on the behavior of the systems. The theoretical basis of these techniques is called confluence and τ-prioritization. The cone and foci techniques are also explained with regard to protocol verification. Chapters 13 and 14 explore verification techniques to validate complex distributed algorithms, including the use of parameterized Boolean equations to verify modal formulas on processes in linear forms.

Part 3, “Semantics,” has only one chapter (15). The formal semantics of mCRL2 and the related formalism are described here. Data specifications and process declarations and formulations are fully explained.

Each chapter in Parts 1 through 3 has a “Historical Notes” section, which summarizes the theoretical development history of the various concepts.

Part 4 contains the appendices and bibliography. There are six appendices (A through F). Appendix A contains the brief tool primer for those who wish to use the online toolset. The equations used to define the built-in data type in mCRL2 are listed in Appendix B. All of the plaintext notation used in the book is related back to the toolset and explained in Appendix C. Appendix D contains a description of the syntax of all of the formalisms. The axioms for processes are described in Appendix E. Finally, answers to the book’s exercises are in Appendix F. There are 184 references in the bibliography, and there is an acceptable index at the end of the book. However, I would have preferred to have all of the acronyms used in the book included in the index.

The authors wrote this book for their graduate-level computer science class. It is a very good textbook when used in combination with the online mCRL2 toolsets, allowing students to perform nontrivial class projects. For practitioners who want to use mCRL2 for system definition and verification, skim Parts 1 and 2 but use Part 3 and the appendices to get familiar with the online toolset in order to use the mCRL2 program.