Finite state description of communication protocols
Gregor von Bochmann · IEEE Computer Society Press eBooks · 1995
Abstract A finite state model for the specification and validation of communication protocols is considered. The concept of “direct coupling” between interactiing finite state components is used to describe a hierarchical structure of protocol layers. The paper discusses different aspects of protocol validation, some verification tools based on the finite state formalism, and the basic limitations of the finite state modelling of protocols. An “empty medium abstraction” is proposed for reducing the complexity of the overall system description. The concept of “adjoint states” can be useful for summarizing the relative synchronization between the communicating system components. These concepts are applied to the analysis of a simple alternating bit protocol, and to the X.25 call set-up and clearing procedures. The analysis of X.25 shows that the procedures are stable in respect to intermittant perturbations in the synchronization of the interface introduced for different reasons, including occasional packet loss. However, on very rare occasions, an undesirable cyclic behaviour could be encountered.