Holzmann G.J. Design and Validation of Computer Protocols

Prentice Hall, 1991. — 560 p.Protocols are sets of rules that govern the interaction of concurrent processes in distributed systems. Protocol design is therefore closely related to a number of established fields, such as operating systems, computer networks, data transmission, and data communications. It is rarely singled out and studied as a discipline in its own right. Designing a logically consistent protocol that can be proven correct, however, is a challenging and often frustrating task. It can already be hard to convince ourselves of the validity of a sequentially executed program. In distributed systems we must reason about concurrently executed, interacting programs.
Books about distributed systems, computer networks, or data communications often do no better than describe a set of standard solutions that have been accepted as correct by, for instance, large international organizations. They do not tell us why the solutions work, what problems they solve, or what pitfalls they avoid.
This text is intended as a guide to protocol design and analysis, rather than as a guide to standards and formats. It discusses design issues instead of applications. Two issues, therefore, are beyond the scope of this text: network control (including routing, addressing, and congestion control) and implementation. There is, however, no shortage of texts on both topics. The design problem is addressed here as a fundamental and challenging issue, rather than as an irritating practical obstacle to the development of reliable communication systems. The aim of the book is to make you familiar with all the issues of protocol validation and protocol design.BasicsProtocol Structure.
Error Control.
Flow Control.
Specification and Modeling
Validation Models.
Correctness Requirements.
Protocol Design.
Finite State Machines.
Conformance Testing, Synthesis and Validation
Conformance Testing.
Protocol Synthesis.
Protocol Validation.
Design Tools
A Protocol Simulator.
A Protocol Validator.
Using the Validator.Data Transmission.
Flow Chart Language.
PROMELA Language Report.
SPIN Simulator Source.
SPIN Validator Source.
PROMELA File Transfer Protocol.