Formal Specifications and Verification of Message Ordering Properties in a Broadcasting System using Event B

Causal and total order broadcast has been proposed as a mechanism to provide fault tolerance for constructing reliable distributed systems. The use of formal methods to develop a model of a system, specifying critical properties and the verification of them is a way of obtaining better design of dependable services. Event B is a formal technique which provides a framework for developing mathematical models of distributed systems by rigorous description of the problem, gradually introducing solutions in the refinement steps, and verification of solutions by discharge of proof obligations. In this paper, we present a formal development of a system in Event B where processes communicate by broadcast and the messages are delivered following a causal and a total order. We first present separate models of a broadcast system each for a causal order and a total order. Subsequently, we verify that the models of the system preserves the required ordering properties. Further, we develop a model of a system satisfying both causal and a total order on the messages. Later in the refinement, we outline how these ordering properties can correctly be implemented by the vector clocks. In this approach we discover some interesting invariant properties which describes the relationship of abstract causal and total order with the vector clocks and the sequence numbers