A Validation Technique for Tightly Coupled Protocols

For several years the authors have been part of an effort developing automated techniques for examining the syntax of protocols for the absence of various errors. Recently, we have turned our attention to trying to prove various functional properties of protocols used in ring-topology systems. Ring systems have a number of properties that distinguish them from the more general computer networks towards which our earlier validation work was directed. We report here on the resulting changes in the protocol models and validation techniques, together with extensions used to prove that the protocol being examined has the various desirable functional properties demanded of it.