More rigorous modeling and proving techniques have been applied with increasing success in communications protocol design. There are two basic ways to go about this.

The more-or-less standard approach, often called the dual-language approach, is to ask the user to express the protocol behavior and the design requirements in two independent formalisms, usually some flavor of finite state machine model for the former and some flavor of temporal logic for the latter. The design verification task then boils down to proving that the temporal logic requirements are satisfied for every conceivable execution of the finite state machine behavior model.

In the second or single-language approach, the user is asked to formalize both the design requirements and the system behavior in a single uniform notation. The effort is now to derive the behavior as much as possible from an initial set of requirements. By a sequence of transformation steps, ultimately, it should thus be possible to derive an implementation from the initial requirements, in part as a simple logical consequence.

This approach is pursued in this paper. It is based on the process algebra Lotos (an ISO international standard), and it discusses a sample of transformation rules that have been proven to preserve certain specific notions of correctness. An impressive array of such transformation rules is available today. An effective toolset supports the Lotos transformation rules. The tools can be used to apply those rules that can be automated, or to verify the correct application of the user-driven rules.

The paper is aimed at readers who have a good working knowledge of the Lotos language. A comparison of the pros and cons of the Lotos approach to protocol design and the classic dual-language approach is not included in the paper, which is somewhat regrettable. The largest problem with both approaches is that a user is typically laxer in formalizing requirements than in formalizing behavior. (After all, the user usually simply “knows” that a design is correct.) In the dual-language approach, this laxness leads to inconsistencies between the behavior and requirement specifications, which can be corrected as part of the regular process of verification. In the single-language approach, an incomplete or inconsistent set of requirements could survive the entire design trajectory. A series of provably correct transformation steps may now be allowed to faithfully reproduce the flaws from the initial requirements, until the complete final implementation is realized. Of course, the further development of both approaches to the protocol design problem is being pursued actively. It is unpredictable which method will turn out to be stronger in the long run.

For those interested in a quick overview of the state of the art in protocol design using formal methods based on Lotos, this paper is definitely recommended reading.