Jason Hickey, Nancy Lynch, Robbert van Renesse. Specifications and Proofs for Ensemble Layers. Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99), Amsterdam, the Netherlands, March 1999. Springer-Verlag. (Compressed Postscript)

Abstract

Ensemble is a widely used group communication system that supports distributed programming by providing precise guarantees for synchronization, message ordering, and message delivery. Ensemble eases the task of distributed application programming, but as a result, ensuring the correctness of Ensemble itself is a difficult problem. In this paper we use I/O automata for formalizing, specifying, and verifying the Ensemble implementation. We focus specifically on message total ordering, a property that is commonly used to guarantee consistency within a process group. The systematic verification of this protocol led to the discovery of an error in the implementation.