Specifications and proofs for ensemble layers

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, ensur- ing the correctness of Ensemble itself is a diffcult problem. In this paper we use I/O automata for formalizing, specifying, and verifying the En- semble 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.