Skip to main content
PRL Project

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)

  • unofficial copies PDF, PS


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

cite link