This paper characterizes and compares five techniques of formal specification of computer network protocols. As the basis of the discussion, each of the five techniques is used to specify one (and the same) so-called alternating bit protocol, a protocol providing reliable communication over an unreliable transmission line by repeated transmission. The five techniques differ with respect to what part of the requirements on the protocol is expressed as restrictions on the current state, and what part is expressed as restrictions on the history of states. At one extreme, the protocol can be specified purely by state transitions. At the other extreme, the procotol is specified purely in terms of allowable sequences of events. The remaining three techniques comprise various mixtures of state and event history descriptions in their requirement formulations. Wherever event history is described, it is expressed in the notation of temporal logic, which is briefly reviewed. Each of the five specifications is supposed to express system requirements described informally by three safety and three liveness properties, and is given as a set of diagrams or formulas accompanied by explanations and comments.

In a final comparison, it is concluded that none of the five techniques are completely satisfying; even for the simple protocol considered, it is difficult to achieve certainty that the specification correctly reflects the abstract requirements. It is stated that “the state transitions diagram form seems to be the easiest to understand.” This statement implies a recognition that the psychological issue of understandability is a significant question in judging specification techniques. However, this question is dealt with no further, which indicates the limitation of the perspective of the study. Clearly, more work on formal specification techniques, dealing also with their psychological aspects, is needed.

The presentation is admirably clear, but in its concentration requires careful study. Unfortunately, the formulas are set in such small print they are partly unreadable. As a whole, the study contrasts very favorably with the all-too-common presentations which make the unwarranted assumption that any form of formalization is a blessing.