Protocol Validation by Duologue-Matrix Analysis

A protocol is a set of rules which governs the interaction between processes. It is difficult to design protocols without errors because there are usually more interactions possible than anticipated. We are concerned with two-process protocols. A technique is described which identifies design errors in protocols. The technique is based on modeling a protocol as a pair of interacting graphs whereby interaction sequences are represented by path pairs (one path in each graph). The technique is currently limited to protocols that must revert to an initial or quiescent state after a finite number of interaction steps. The work represents a theory that can be automated on a digital computer.