Towards Analyzing and Synthesizing Protocols

Abstract

The production of error-free protocols or complex process interactions is essential to reliable communications. This paper presents techniques for both the detection of errors in protocols and for prevention of errors in their design. The methods have been used successfully to detect and correct errors in existing protocols. A technique based on a reachability analysis is described which detects errors m a design. This "perturbation technique" has been implemented and has successfully detected inconsistencies or errors in existing protocol designs including both X.21 and X.25. The types of errors handled are state deadlocks, unspecified receptions, nonexecutable interactions, and state smbiguities. These errors are discussed and their effects considered. An interactive design technique is then described that prevents design errors. The technique is based on a set of production rules which guarantee that complete reception capability is provided in the interacting processes. These rules have been implemented in the form of a tracking algorithm that prevents a designer from creating unspecified receptions and nonexecutable interactions and monitors for the presence of state deadlocks and ambiguities.