Formal specification of asynchronous checkpointing using Event-B

The major issue in distributed systems is the recovery from some short term failures. It is desired to have transparent scheme for recovery, from such failures, which is efficient as well. Checkpoint is the one of the scheme. Checkpoint-based protocols simply depend on checkpointing in order to get system state restoration. Generally, checkpointing may be categorised as synchronous, asynchronous or communication-induced. While, there is another mechanism, log-based, in which checkpointing also include logging of nondeterministic events. These events are encoded in tuples known as determinants. A formal reasoning is required to precisely understand the behaviour of such techniques and to understand how they achieve the objectives. Event-B is a formal technique which gives a framework for the distributed systems by mathematical models. We are presenting a formal development of asynchronous checkpointing using Event-B in this paper.