Formal Specification and Verification of Total Order Broadcast through Destination Agreement Using Event-B

A reliable broadcast is communication primitive used to develop fault tolerant distributed applications. It in due course delivers messages to all participating sites irrespective of their ordering. Total order broadcast impose restriction on message ordering and satisfies total order requirement.

A clear specifications, rigorous validation and verification is key to obtain better design of dependable services in such applications. With the help of formal methods one can specify and verify systems in systematic rather than ad hoc manner. It reveals ambiguities, incompleteness, and inconsistencies in a system by facilitating clear specification, rigorous validation and verification.

In this paper, we present a formal development of total order broadcast. The model have been developed and checked by using event-B techniques supported by the RODIN tool. Event-B is a formal technique that supports the incremental design of a distributed applications using notion of refinements.