The application of distributed systems is ubiquitous in almost every facet of today’s computerized life. Systems with various architecture configurations, including peer-to-peer (P2P), multi-tier (n-tier), and client-server, can be identified virtually anywhere, from banking, communication, and transportation to entertainment and education. While the application and use of distributed systems lends itself to exploring exciting new areas for discovery, the theoretical underpinnings of this area are complex, and mastery of the underlying theory is hard to achieve.
Fokkink deals with the theoretical underpinnings of distributed systems. The title, perhaps somewhat deceiving as it leaves open the possibility that this is a book about the simulation of distributed systems, is otherwise accurate. This textbook contains an excellent survey of prominent formal verification and modeling techniques using algebraic specification and verification of distributed systems. As described in the preface, the book is a compilation of lecture notes for a graduate-level course in protocol validation. The level and scope of the material is clearly at an advanced level, so it is not recommended for the casual reader. However, the material is well written and clearly presented.
The author’s writing style is crisp, and the structure of the book is well organized. The first few chapters cover abstract data types and process algebra. This is done using the µCRL process algebraic language. µCRL was developed to take data into account during the study of communicating processes, so the language describes and analyzes distributed systems. Subsequent chapters examine such topics as external process transitions, and specifications of standard protocols and their transformation. The book concludes with symbolic verification techniques and an appendix with a useful synopsis of the µCRL tool set.
The eight chapters are well structured. While they can be read independently, they build on each other in a way that is easy to follow. The flow of the text is smooth, with clear definitions and figures when necessary. Despite the theoretical content, theorems and proofs are absent, which actually enhances readability since they typically work as reading “speed bumps.” Each chapter has relevant exercises that reinforce the content, and examples are used to illustrate key points.
The book would be ideal for instructional use, as it provides an overview of algebraic specification and verification of distributed systems on the basis of a modern verification tool. For instructors, the material is readily available to be presented to students. Using the author’s style and structure, instructors may easily expand and develop their own protocol-verification examples. Another nice feature of the book is the set of solutions for the chapter exercises. The book also contains an index and ample references to a rich bibliography that instructors, students, and researchers will find very useful. Physically, this 150-page book is relatively small in size, but it is packed with a solid, well-organized, and well-written examination of its topic. I highly recommend this book for the advanced study of the modeling and verification of distributed systems.