Formal Specification & Verification of Checkpoint Algorithm for Distributed Systems using Event - B

摘要

Using formal methods to design a system model, and then specifying and verifying critical properties of that model is a way to design safety critical systems. Modeling can be done by a proper methodology so that one can analyze proposed behavior of the models quantitatively. Formal method used to develop the distributed system models is Event B. This approach consists of meticulously defining the problem in a conceptual model, incorporating problem solutions or design information in the refinement steps for the sake of obtaining concrete requirements, and checking the accuracy of explanations offered. The existing B tools offer substantial automatic proof assistance to generate and discharge the proof obligations. The various processes at different locations are linked by the network in a distributed system. They communicate with each other by sending messages. A checkpoint is a process’s saved local state. If the global state created by the saved states is consistent, a collection of checkpoints, one per system process, is consistent. In this paper a refined methodology is introduced for the development of distributed system models using EventB, in which processes coordinate their checkpoint through broadcasting messages to always create a consistent set of checkpoints. A formal logic method is needed to understand the behavior of these techniques and achieve the goals.