DESIGN AND VALIDATION OF COMPUTER PROTOCOLS
By: Gerard J. Holzmann, Prentice-Hall, 1991
A protocol specification consists of five distinct parts. To be complete, each specification should include explicitly:
1. The service to be provided by the protocol
2. The assumptions about the environment in which the protocol is executed
3. The vocabulary of messages used to implement the protocol
4. The encoding (format) of each message in the vocabulary
5. The procedure rules guarding the consistency of message exchanges
A designer will adhere to the discipline only if in return, provably and reproducibly, a more reliable product can be obtained. Below we give an overview of what is likely to become part of a general set of principles of sound design, which will allow us to enter the second phase of development in the field of protocol engineering. It is important to recognize that all these notes are variations on two common themes: simplicity and modularity.
SIMPLICITY — THE CASE FOR LIGHT-WEIGHT PROTOCOLS
A well-structured protocol can be built from a small number of well-designed and well-understood pieces. Each piece performs one function and performs it well. To understand the working of the protocol it should suffice to understand the working of the pieces from which it is constructed and the way in which they interact. Protocols that are designed in this way are easier to understand and easier to implement efficiently, and they are more likely to be verifiable and maintainable. A light-weight protocol is simple, robust, and efficient. The case for light-weight protocols directly supports the argument that efficiency and verifiability are not orthogonal, but complementary concerns.
MODULARITY — A HIERARCHY OF FUNCTIONS
A protocol that performs a complex function can be built from smaller pieces that interact in a well-defined and simple way. Each smaller piece is a light-weight protocol that can be separately developed, verified, implemented, and maintained. Orthogonal functions are not mixed; they are designed as independent entities. The individual modules make no assumptions about each other’s working, or even presence. Error control and flow control, for instance, are orthogonal functions. They are best solved by separate light-weight modules that are completely unaware of each other’s existence. They make no assumptions about the data stream other than what is strictly necessary to perform their function. An error-correction scheme should make no assumptions about the operating system, physical addresses, data encoding methods, line speeds, or time of day. Those concerns, should they exist, are placed in other modules, specifically optimized for that purpose. The resulting protocol structure is open, extendible, and rearrangeable without affecting the proper working of the individual components.
A well-formed protocol is not over-specified, that is, it does not contain any unreachable or unexecutable code. A well-formed protocol is also not under-specified or incomplete. An incompletely specified protocol, for instance, may cause unspecified receptions during its execution. An unspecified reception occurs if a message arrives when the receiver does not expect it or cannot respond to it.
A well-formed protocol is bounded: it cannot overflow known system limits, such as the limited capacity of message queues.
A well-formed protocol is self-stabilizing. If a transient error arbitrarily changes the protocol state, a self-stabilizing protocol always returns to a desirable state within a finite number of transitions, and resumes normal operation. Similarly, if such a protocol is started in an arbitrary system state, it always reaches one of the intended states within finite time.
A well-formed protocol, finally, is self-adapting. It can adapt, for instance, the rate at which data are sent to the rate at which the data links can transfer them, and to the rate at which the receiver can consume them. A rate control method, for instance, can be used to change either the speed of a data transmission or its volume.
As Polybius (Chapter 1) noted,
‘‘it is chiefly unexpected occurrences which require instant consideration and help.’’
It is not difficult to design protocols that work under normal circumstances. It is the unexpected that challenges them. It means that the protocol must be prepared to deal appropriately with every feasible action and with every possible sequence of actions under all possible conditions. The protocol should make only minimal assumptions about its environment to avoid dependencies on particular features that could change. Many link-level protocols that were designed in the 1970s, for instance, no longer work properly if they are used on very high speed data lines (in the Gigabits/sec range). A robust design automatically scales up with new technology, without requiring fundamental changes. The best form of robustness, then, is not over-design by adding functionality for anticipated new conditions, but minimal design by removing non-essential assumptions that could prevent adaptation to unanticipated conditions.
There are some standard and dreaded ways in which protocols can fail. We list three of the more important ones.
In general, the observance of these criteria cannot be verified by a manual inspection of the protocol specification. More powerful tools are needed to prevent or detect them. Such tools are discussed in Part III.
The principles discussed above lead to ten basic rules of protocol design.
The most frequently violated rule, clearly, is Rule 10.