A compositional approach for designing protocols

The complexity of designing distributed protocols has led to compositional techniques for designing and verifying protocols. The author proposes a technique based on the notion of parallel composition of protocols. It allows the component protocols to share messages and variables. The composite protocol is an interleaved execution of the component protocols with the constraint that they be synchronized at events updating shared variables or sending/receiving shared messages. All invariants of the component protocols are preserved in the composite protocol. The technique allows modular design and verification of protocols. It can be viewed as an inverse of the projection method for verifying protocols