Formal Aspects of Computing (1996) 8:498 9 1996 BCS

Formal Aspects of Computing

BOOK REVIEW Algebraic Specification of Communication Protocols. S. Mauw and G. J. Veltink (editors), Cambridge

Tracts in Theoretical Computer Science 36, Cambridge University Press, 1993, ISBN 0-521-41883-6 One of the problems of formal methods is that while many are keen to promote their particular formalism, often there is a lack of good example specifications to allow practitioners to judge for themselves the merits of a formalism. This book attempts to increase awareness of formal methods, in particular PSF (Process Specification Formalism), and the benefits of using formal methods by presenting a number of graded specifications in the field of communications protocols. This book follows the tradition of earlier books in the CUP Tracts in Theoretical Computer Science Series from the same school of specification (numbers 17 and 18 on Process Algebra and Applications of Process Algebra respectively). The book begins with a very clear introduction to the ideas underlying the use of formal methods and also the ideas underlying ISO (International Standards Organisation) communications protocols. This is followed by an introduction to the PSF language and its associated toolkit and libraries. The remainder of the book consists of communications protocol specifications. We progress from very simple protocols, such as the Alternating Bit protocol, through variations on Sliding Window Protocols to simplified versions of the Token Ring Protocol and Ethernet (CSMA/CD) Protocol. In all except the final specification the bulk of technical detail is abstracted away to allow for a clearer, more high-level, presentation. Finally, appendices provide the full PSF libraries and syntax of the language, a full reference list pointing towards further reading, and a nice index covering both keywords and module names of the PSF specifications. The style of the introduction to PSF I found rather annoying. The examples are given before the explanation of each operator, leaving me feeling that I was working out the semantics of each operator myself from the clues in the example, only to then go on to read about the operator. I also did not like the way the references are discussed only at the end of each chapter, rather than citing references at the appropriate point in the main text. Both of these matters are largely matters of personal preference. Students, for example, may prefer the text to be uncluttered by references. These are also fairly minor quibbles; the most important part of the book is concerned with the actual specifications. Each example in the book is described in a similar manner; first an informal description of the system is given, followed by the formal PSF specification. PSF is modular, which allows the specification to be broken down into small, easily digestible, chunks; the authors include plenty of informal comment with the specifications, which helps to illuminate the bare specification. Although the style is consistent on the whole, a notable exception is the last chapter on the Token Ring Protocol which had a slightly different style. More importantly, this chapter is not tied to the presentation of the simplified token ring protocol in the previous chapter, a rather strange omission. The chapter on sliding window protocols is particularly nice; starting with a very simple sliding window protocol we progress, by varying aspects of the protocol, to a more complicated version. This is followed by a discussion on the external behaviour of the different versions of the protocol which underlines the differences and similarities between them. The book achieves what it set out to do, i.e. to provide a set of studies in specification using PSF, using real world examples. Thanks to the clear presentation these studies certainly will help promote formal methods to the wider community. It would make a good library reference, or could perhaps be used in conjunction with a formal methods or a communications course. The clear presentation is well suited for people trying to learn either topic. Note also that it is not necessarily restricted to PSF; due to the similarities between PSF and other process algebras the examples could be easily adapted to e.g. CCS or LO-TOS. For this reason the book could also be used by the academic community as a source of standard case studies in communications protocols. Personally, it would have been nice to see more done with the specifications. For example, we are told all about the PSF toolkit, but it is never used in the examples, and the topic of verification is only very briefly covered. Perhaps this is to be the subject of another book? If so, I look forward to it greatly. Carton Kirkwood Glasgow Please send books for review to Professor UHM Martin, Computational Science Division, University of St Andrews, St Andrews, Fife, Scotland KY16 6SS, UK