Alan Fekete, Nancy Lynch, and Alex Shvartsman. Specifying and Using a Partitionable Group Communication Service. Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing (PODC'97, Santa Barbara, CA), pages 53-62, August 1997. .pdf Also, Technical Memo MIT/LCS/TM-570, Laboratory for Computer Science, Massachusetts Institute of Technology, October 1997. .pdf

Abstract

A new, simple formal specification is presented for a partitionable view-oriented group communication service. The specification consists of a state machine to express safety requirements and a timed trace property to express performance and fault-tolerance requirements. The specification is used to construct a totally-ordered-broadcast application, using an algorithm (based on algorithms of Amir, Dolev, Keidar and others) that reconciles information derived from different views of the group. Correctness of the resulting application is proved, and its performance and fault-tolerance analyzed. The specification has a simple implementation, based on a group membership algorithm of Cristian and Schmuck.