Formal Verification of Distributed Checkpointing Using Event-B

The development of complex system makes challenging task for correct software development. Due to faulty specification, software may involve errors. The traditional testing methods are not sufficient to verify the correctness of such complex system. In order to capture correct system requirements and rigorous reasoning about the problems, formal methods are required. Formal methods are mathematical techniques that provide precise specification of problems with their solutions and proof of correctness. In this paper, we have done formal verification of check pointing process in a distributed database system using Event B. Event-B is an event driven formal method which is used to develop formal models of distributed database systems. In a distributed database system, the database is stored at different sites that are connected together through the network. Checkpoint is a recovery point which contains the state information about the site. In order to do recovery of a distributed transaction a global checkpoint number (GCPN) is required. A global checkpoint number decides which transaction will be included for recovery purpose. All transactions whose timestamp are less than global checkpoint number will be marked as before checkpoint transaction (BCPT) and will be considered for recovery purpose. The transactions whose timestamp are greater than GCPN will be marked as after checkpoint transaction (ACPT) and will be part of next global checkpoint number.