Design and Validation of Computer Protocols

Design and Validation of Computer Protocols was published by Prentice Hall in November 1990. Among others, it details the design and implementation of the Spin model checking system.

Prentice Hall, 1991, 512 pgs.
ISBN 0-13-539925-4 hardcover (USA)
ISBN 0-13-539834-7 paperback (international edition)

Source to all examples from the book is available as a tarfile: examples.tar (90Kb).

Availability (new)

Although the book has been officially out of print for a good number of years, on-demand printed
paperback copies of the book can still be ordered (for around $80) from amazon.com.

An updated version of the complete book is also available in electronic form (for $10 through paypal) from this website.


A more recent book on the Spin model checker is also available, though not in PDF form. (e.g., from amazon.com).


Book Overview

A review of the book appeared in ACM SIGCOMM Computer Communications Review, Vol. 21, Issue 2 (April 1991), p. 14. It writes, in part:


The book introduces a discipline for the design of concurrent systems. The techniques have been applied to the design of distributed systems, operating systems, telephone switching systems, and network protocols, but they are not restricted to any particular application. With the software verification tools presented in this book, formal validations of industrial-size problems can be performed effectively.

The first part of the book gives the reader an overview of the types of fundamental coordination problems that a protocol designer must be able to recognize. It covers the basics of error control, flow control, and protocol structuring, and presents ten basic rules of protocol design. Part two covers protocol specification and modeling techniques, and introduced the notion of a protocol validation model. Part three gives an overview of protocol synthesis, conformance testing, manual and automated protocol validation techniques. In the final part of the book a detailed description is given of a set of tools that can be used to attack the protocol design problem in a rigorous and practical manner. Complete source code for the tools is provided, and is also available freely for downloading from this website (www.spinroot.com).


[Selected parts from the book, such as the foreword, preface, chapters 1 and 8, and the name and subject index, are available for download freely for preview, via the links provided below.]

Table of Contents

Foreword ix

Preface xi

Part I -- Basics

1. Introduction

2. Protocol Structure

3. Error Control

4. Flow Control

Part II -- Specification and Modeling

5. Validation Models

6. Correctness Requirements

7. Protocol Design

8. Finite State Machines

Part III -- Conformance Testing, Synthesis and Validation

9. Conformance Testing

10. Protocol Synthesis

11. Protocol Validation

Part IV -- Design Tools

12. A Protocol Simulator

13. A Protocol Validator

14. Using the Validator

Conclusion 350

References 351

Appendices



author
spinroot.com