Specifying and Proving Communication Closedness in Protocols

摘要

The principle of communication closed layers by Eltrad and Francez has been shownto be very useful in the design of distributed protocols and algorithms. In the paper the authors investigate the communication closed layers principle as an algebraic law with syntactic side conditions. Although these side conditions seem to put limits to the applicability the authors show that by means of multiplexing and data refinement techniques they can enlarge the scope of the law to numerous examples, including the derivation of a Two Phase Commit protocol and the Gallagher, Humblet, and Spira algorithm for minimum weight spanning trees. The authors also discuss the relation to more general formulations of the principle of communication closed layers by means of temporal logics and the relation between partial order temporal logics and the authors' process language.