Specifications and Proofs for Ensemble Layers

unofficial copies [PDF], [PS]


by Jason Hickey, Nancy Lynch, and Robbert van Renesse

Proceedings of Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), R. Cleaveland (ed.), LNCS 1579, pp. 119-133, Springer-Verlag, 1999.

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.