On the Algebraic Synthesis of Protocols.pdfVIP

On the Algebraic Synthesis of Protocols Gerard J. Holzmann Bell Laboratories Murray Hill, New Jersey 07974 ABSTRACT A simple algebraic notation is used to derive a protocol specification from a for- malized description of a data link. The goal of the protocol will be reliable data transfer by correcting for the potentially erroneous behavior of a channel. 1. Introduction One of the toughest open problems in the area of protocol verification is to find analytical models with suf- ficient descriptive power to model the main characteristics of a protocol, and yet with sufficient analytical power to allow us to prove interesting properties about it. The requirements conflict. There are models with sufficient descriptive power (programming languages) that are hard to verify. There are also models that can be analyzed (e.g. Petri Nets), but cannot adequately model the protocol properties we are interested in. Adding descriptive power makes the analyses intractable; removing it makes them irrelevant. Within the limits of the problem as stated here, progress has been made in the construction of tools that can offer practical help to a protocol designer in proving protocols correct [e.g. Zafi ’80, Blum ’82, Holz ’85, Nounou ’86]. Most of these tools, though, require us to construct the model of the protocol being validated as a separate entity: the model cannot usually be derived from the implementation, nor can an implementa- tion easily be derived from a model that was proven correct. Unintended idealizations in the model may then mislead the programmer on the correctness of his design. Similarly, simpli