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:
Overall, this book is an important contribution, and introduction, to the science of protocol design .
To my knowledge no comparable text exist. I recommend its use in, for example, a course on protocol
design. A more experienced practitioner will find Holzmann's work both useful and inspiring.
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
Part I -- Basics
- 1.1 Early Beginnings 1
- 1.2 The First Networks 9
- 1.3 Protocols as Languages 12
- 1.4 Protocol Standardization 13
- 1.5 Summary 15
- Exercises 16
- Bibliographic Notes 17
2. Protocol Structure
- 2.1 Introduction 19
- 2.2 The Five Elements of a Protocol 21
- 2.3 An Example 22
- 2.4 Service and Environment 27
- 2.5 Vocabulary and Format 32
- 2.6 Procedure Rules 35
- 2.7 Structured Protocol Design 36
- 2.8 Ten Rules of Design 39
- 2.9 Summary 40
- Exercises 40
- Bibliographic Notes 41
3. Error Control
- 3.1 Introduction 43
- 3.2 Error Model 44
- 3.3 Types of Transmission Errors 46
- 3.4 Redundancy 46
- 3.5 Types of Codes 47
- 3.6 Parity Check 48
- 3.7 Error Correction 49
- 3.8 A Linear Block Code 52
- 3.9 Cyclic Redundancy Checks 57
- 3.10 Arithmetic Checksum 63
- 3.11 Summary 64
- Exercises 65
- Bibliographic Notes 66
4. Flow Control
- 4.1 Introduction 67
- 4.2 Window Protocols 71
- 4.3 Sequence Numbers 75
- 4.4 Negative Acknowledgments 82
- 4.5 Congestion Avoidance 84
- 4.6 Summary 88
- Exercises 88
- Bibliographic Notes 90
Part II -- Specification and Modeling
5. Validation Models
- 5.1 Introduction 91
- 5.2 Processes, Channels, Variables 92
- 5.3 Executability of Statements 92
- 5.4 Variables and Data Types 93
- 5.5 Process Types 94
- 5.6 Message Channels 98
- 5.7 Control Flow 101
- 5.8 Examples 104
- 5.9 Modeling Procedures and Recursion 105
- 5.10 Message Type Definitions 106
- 5.11 Modeling Timeouts 106
- 5.12 Lynch's Protocol Revisited 107
- 5.13 Summary 109
- Exercises 109
- Bibliographic Notes 111
6. Correctness Requirements
- 6.1 Introduction 112
- 6.2 Reasoning about Behavior 113
- 6.3 Assertions 116
- 6.4 System Invariants 116
- 6.5 Deadlocks 118
- 6.6 Bad Cycles 119
- 6.7 Temporal Claims 120
- 6.8 Summary 126
- Exercises 126
- Bibliographic Notes 127
7. Protocol Design
- 7.1 Introduction 128
- 7.2 Service Specification 129
- 7.3 Assumptions about the Channel 130
- 7.4 Protocol Vocabulary 131
- 7.5 Messsage Format 133
- 7.6 Procedure Rules 141
- 7.7 Summary 160
- Exercises 161
- Bibliographic Notes 162
- 8.1 Introduction 163
- 8.2 Informal Description 163
- 8.3 Formal Description 171
- 8.4 Execution of Machines 172
- 8.5 Minimization of Machines 173
- 8.6 The Conformance Testing Problem 176
- 8.7 Combining Machines 176
- 8.8 Extended Finite State Machines 177
- 8.9 Generalization of Machines 180
- 8.10 Restricted Models 183
- 8.11 Summary 186
- Exercises 187
- Bibliographic Notes 187
Part III -- Conformance Testing, Synthesis and Validation
9. Conformance Testing
- 9.1 Introduction 189
- 9.2 Functional Testing 190
- 9.3 Structural Testing 191
- 9.4 Deriving UIO Sequences 197
- 9.5 Modified Transition Tours 199
- 9.6 An Alternative Method 199
- 9.7 Summary 201
- Exercises 202
- Bibliographic Notes 203
10. Protocol Synthesis
- 10.1 Introduction 206
- 10.2 Protocol Derivation 206
- 10.3 Derivation Algorithm 211
- 10.4 Incremental Design 213
- 10.5 Place Synchronization 213
- 10.6 Summary 214
- Exercises 215
- Bibliographic Notes 215
11. Protocol Validation
- 11.1 Introduction 217
- 11.2 Manual Proof Method 217
- 11.3 Automated Validation Methods 221
- 11.4 The Supertrace Algorithm 230
- 11.5 Detecting Non-Progress Cycles 235
- 11.6 Detecting Acceptance Cycles 238
- 11.7 Checking Temporal Claims 239
- 11.8 Complexity Management 240
- 11.9 Boundedness of PROMELA Models 242
- 11.10 Summary 243
- Exercises 244
- Bibliographic Notes 244
Part IV -- Design Tools
12. A Protocol Simulator
- 12.1 Introduction 247
- 12.2 SPIN -- Overview 248
- 12.3 Expressions 249
- 12.4 Variables 259
- 12.5 Statements 269
- 12.6 Control Flow 278
- 12.7 Process and Message Types 285
- 12.8 Macro Expansion 294
- 12.9 SPIN Options 295
- 12.10 Summary 297
- Exercises 298
- Bibliographic Notes 298
13. A Protocol Validator
- 13.1 Introduction 298
- 13.2 Structure of the Validator 299
- 13.3 The Validation Kernel 300
- 13.4 The Transition Matrix 303
- 13.5 The Validator-Generator Code 305
- 13.6 Overview of the Code 308
- 13.7 Guided Simulation 310
- 13.8 Some Applications 311
- 13.9 Coverage in Supertrace Mode 315
- 13.10 Summary 316
- Exercises 316
- Bibliographic Notes 317
14. Using the Validator
- 14.1 Introduction 318
- 14.2 An Optical Telegraph Protocol 318
- 14.3 Dekker's Algorithm 320
- 14.4 A Larger Validation 322
- 14.5 Flow Control Validation 325
- 14.6 Session Layer Validation 336
- 14.7 Summary 348
- Exercises 349
- Bibliographic Notes 349
Conclusion 350
References 351
Appendices
- A. Data Transmission 369
- B. Flow Chart Language 382
- C. PROMELA Language Report 385
- D. SPIN Simulator Source 394
- E. SPIN Validator Source 433
- F. PROMELA File Transfer Protocol 483
- Name Index 491
- Subject Index 493
author
spinroot.com