A General Transition Model for Protocols and Communication Services

Different approaches have been used for the formal specification and verification of communication protocols. This paper explains the approach of nsing a general transition model which combines aspects of finite state transition diagrams and programming languages. Different ways of structuring a protocol into separate modules or functions are also discussed. The main part of the paper describes a method for exactly specifying the communication service provided by a protocol. Two aspects of a service specification are distinguished: 1) the local properties which characterize the interface through which the service may be accessed, and 2) the global properties which describe the "end-to-end" communication characteristics of the service. It is shown how the specification method is related to the general transition model for protocol specification. Verification is discussed briefly with emphasis on the use of invariant assertions in the context of finite state as well as programming language protocol descriptions. The discussed topics are demonstrated with examples based on the HDLC classes of procedures and the X.25 Virtual Circuit data transmission service.