With over two decades’ experience in the development, deployment, and user of computer networks, a large number of textbooks in this field have been written. Those on protocol design usually emphasize performance modeling and analysis in terms of such parameters as overhead, throughput, or delay. It is refreshing to see this new book, which takes the correctness of a protocol as its focus.

The book contains four parts. The first covers the basics of protocol design and the types of design problems to be dealt with. It provides a brief account of protocol structuring and design principles (chapter 2), error control (chapter 3), and flow control (chapter 4). Part 2 discusses formal protocol specification and modeling techniques. It presents a language called PROMELA, developed by the author for the description of protocol validation models (chapter 5) and the specification of protocol correctness requirements (chapter 6). The use of this language is illustrated by the design of a simple file transfer protocol (chapter 7), and PROMELA’s relationship to the finite state machine model is discussed (chapter 8). Part 3 gives an overview of conformance testing (chapter 9), protocol synthesis (chapter 10), and protocol validation techniques (chapter 11). In the final part, a set of PROMELA-based protocol design tools is described in detail. These include a protocol simulator called SPIN (chapter 12) and a protocol validator (chapter 13). These tools are applied to validate the PROMELA-specified file transfer protocol (chapter 14). In the appendices, complete source code for the tools is provided.

Because of the complexity of the interactions of concurrent processes in distributed systems, it is challenging to ensure that a protocol designed for such interactions is logically consistent and complete. It is even more difficult to prove that such a protocol is correct. Manual proofs are not only tedious and time consuming, they are inevitably susceptible to human errors. A central theme of the book is that automated tools are needed to aid the design task and that such tools are now ready to handle real-world protocols.

A key concept for the tool-based design discipline developed in the book is an implementation-independent validation model that expresses the essential characteristics of a protocol in terms of process interactions. Automated tools can interpret such validation models and uncover design flaws. The contents of the book are organized around this concept. The author leads the reader step by step through the issues of protocol validation by presenting the PROMELA language, showing how it can be used to specify the file transfer protocol, explaining the strategies to attack the state space explosion problem in the development of an automated validation tool system, and finally using this system to validate the file transfer protocol.

The book is well organized and the author has given an excellent description of his work, particularly the supertrace algorithm, and the tools that he developed. The author describes work done by others only in a cursory manner, however. Although the author ends each chapter with bibliographic notes to guide the reader to probe further, I would like a more in-depth tutorial survey of the state of the art in the subject. Despite this, I would recommend this book for both students and professionals in the field.