An Automated Technique of Communications Protocol Validation

An interaction between two communicating processes can be defined in terms of a protocol or set of rules governing the exchange of messages between them. For any given protocol, it is a significant problem to determine whether or not errors can occur when the processes interact. In this paper, we describe an implementation of a recent theory of Zafiropulo, which defines protocols in terms of the interaction between two directed graphs, and uses set theory and predicate logic to determine all error conditions that can arise. The overall structure of the theory is used, but the determination of the error conditions is based on a graphical representation of the interaction, and particular emphasis is placed on the state of the channel between the two processes. The technique is currently limited to the validation of two-process protocols in which the processes return to an initial state after a finite number Of interaction steps. The implementation demonstrates that a completely automated procedure can be defined which finds a significant class of errors in communications protocols.