Formal development of Byzantine immune total order broadcast system using event-B

Abstract

A reliable broadcast eventually delivers messages to all participating sites. A total order broadcast is a stronger notion of a reliable broadcast that deliver messages to all processes in a same delivery order. A formal rigorous reasoning is required to precisely understand behaviour of such techniques and an assurance is required to understand how they achieve the objectives. Event-B is a formal technique used for specifying and reasoning about complex systems. In this technique, a system is developed incrementally by adding more details in refinement to obtain more concrete specifications. In this paper, we present a formal development of Byzantine immune total order broadcast system using Event-B. We outline an abstract model specifying total order broadcast using fixed sequencer and introduce more details at refinement level for moving sequencer and detection of Byzantine sequencer. © 2012 Springer-Verlag.