A Proof Technique for Liveness Properties of Multifunction Composite Protocols

In protocol composition techniques, component protocols are combined in various ways to obtain a complex protocol whose execution sequences consist of interleaved execution sequences of the component protocols. In this paper, we investigate the problem of verifying liveness properties of the composite protocol from the known properties of its components. We rst characterize a class of composition techniques that encompasses almost all composition techniques that have appeared in the literature. We then develop a su cient condition to ensure that certain liveness properties of the component protocols carry over to the composite protocol. A proof technique, based on this su cient condition, is then used to determine whether the liveness properties of the component protocols also hold for the composite protocol. To demonstrate the usefulness of our technique, we use several protocols including synchronizing, ordering and disabling protocols as examples. The technique is applicable to any...

• Type: Conference
• Year: 1998
• Where: ICNP
• Authors: J. Park, R. Miller
• Keywords: Component Protocols, Composite Protocol, Composition Techniques, Computer Networks, ICNP 1998