Constructing protocol converters with guaranteed service

The authors consider the conformity property, i.e. that the protocol converters providing communication between different networks meets the service specified by the designer, in constructing protocol converters. Using the top-down approach, an algorithm consisting of the following five steps is proposed to construct a protocol converter: (1) construction of a system graph from the given input; (2) removal of states and transitions that violate the synchronization requirements from the system graph constructed previously; (3) enforcement of liveness requirement on the system graph; (4) verification of the system graph against the service specification; and (5) derivation of a protocol converter from the system graph. The protocol converter so constructed is guaranteed not only to satisfy the conformity property, but also to be free from both deadlock and livelock