Specifications and Proofs for Ensemble Layers
by Jason Hickey, Nancy Lynch, Robbert van Renesse
Proceedings of Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99)
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.
bibTex ref: HLV99