Formal Development of a Fault Tolerant Distributed Checkpoint Process Using Event-B

Abstract

It is really a challenging effort to develop and verify the distributed fault tolerant system. This is because of the communication primitives available for distributed system are not very strong. In Distributed systems processes cooperate and communicate with each other by message exchange. Fault tolerant broadcast mechanisms are must for the construction of the reliable Distributed system. We can achieve the fault tolerance by introducing the Total and causal order broadcast. Use of formal approaches allows us to build fault tolerant distributed systems. In this article, we introduce a systematic system development in which processes communicate through broadcast and messages are exchanged using a total order broadcast mechanism. Total order broadcast primitives were proposed to enable broadcasting system for checkpoint process and allow fault-tolerant co-operation in a distributed network between the sites. We explain how an Event-B refinement-based methodology can be used for the systematic creation of Checkpoint process using total order broadcast models. We introduce a model of broadcasting system for total order and then ensure that the model maintains appropriate ordering attributes while taking the checkpoints. Consequently, in a succession of refinement stages we illustrate how to accurately integrate an abstract total order utilizing the concept of sequence number. This approach allows one to discharge proof obligations due to consistency and refinement checking. To fulfil the proof obligations, it is necessary to find out invariant which define the interconnection among the abstract total order and the process responsible for it.