Formal Specification & Verification of Checkpoint Algorithm for Distributed Systems using Event - B
|International Journal of Engineering Trends and Technology (IJETT)||
|© 2021 by IJETT Journal|
|Year of Publication : 2021|
|Authors : Bal Krishna Saraswat, Raghuraj Suryavanshi, Divakar Yadav
|DOI : 10.14445/22315381/IJETT-V69I4P201|
MLA Style: Bal Krishna Saraswat, Raghuraj Suryavanshi, Divakar Yadav "Formal Specification & Verification of Checkpoint Algorithm for Distributed Systems using Event - B" International Journal of Engineering Trends and Technology 69.4(2021):1-9.
APA Style:Bal Krishna Saraswat, Raghuraj Suryavanshi, Divakar Yadav. Formal Specification & Verification of Checkpoint Algorithm for Distributed Systems using Event - B International Journal of Engineering Trends and Technology, 69(4),1-9.
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 Event-B, 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.
 J. Abrial. The b-book: assigning programs to meanings cambridge university press, 1996.
 J.-R. Abrial. Extending b without changing it (for developing distributed systems). In 1st Conference on the B method, volume 11, 1996.
 J.-R. Abrial. A system development process with event-b and the rodin platform. In International Conference on Formal Engineering Methods, pages 1–3. Springer, 2007.
 J.-R. Abrial and J.-R. Abrial. The B-book: assigning programs to meanings. Cambridge University Press, 2005.
 J.-R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta, and L. Voisin. Rodin: an open toolset for modelling and reasoning in event-b. International journal on software tools for technology transfer, 12(6):447–466, 2010.
 J.-R. Abrial, M. Butler, S. Hallerstede, and L. Voisin. An open extensible tool environment for event-b. In International Conference on Formal Engineering Methods, pages 588–605. Springer, 2006.
 J.-R. Abrial, D. Cansell, and D. M´ery. A mechanically proved and incremental development of ieee 1394 tree identify protocol. Formal aspects of computing, 14(3):215–227, 2003.
 D. Y. Bal Krishna Saraswat, Raghuraj Suryavanshi. A comparative study of checkpointing algorithms for distributed systems. International Journal of Pure and Applied Mathematics, 118:1595–1603, 2018.
 R. Banach. Retrenchment for event-b: Usecase-wise development and rodin integration. Formal Aspects of Computing, 23(1):113– 131, 2011.
 D. Basin, A. F¨urst, T. S. Hoang, K. Miyazaki, and N. Sato. Abstract data types in event-b-an application of generic instantiation. arXiv preprint arXiv:1210.7283, 2012.
 J.-L. Boulanger. Formal methods applied to complex systems: implementation of the B method. John Wiley & Sons, 2014.
 M. Butler and D. Yadav. An incremental development of the mondex system in event-b. Formal Aspects of Computing, 20(1):61–77, 2008.
 K. M. Chandy and L. Lamport. Distributed snapshots: Determining global states of distributed systems. ACM Transactions on Computer Systems (TOCS), 3(1):63–75, 1985.
 Clearsy. B4free tool homepage. www.b4free.com.
 E. N. Elnozahy, L. Alvisi, Y.-M. Wang, and D. B. Johnson. A survey of rollback-recovery protocols in message-passing systems. ACM Computing Surveys (CSUR), 34(3):375–408, 2002.
 S. Hallerstede. Justifications for the event-b modelling notation. In International Conference of B Users, pages 49–63. Springer, 2007.
 M. Jandl, A. Szep, R. Smeikal, and K. M. G¨oschka. Increasing availability by sacrificing data integrity-a problem statement. In Proceedings of the 38th Annual Hawaii International Conference on System Sciences, pages 291c–291c. IEEE, 2005.
 S. Kalaiselvi and V. Rajaraman. A survey of checkpointing algorithms for parallel and distributed computers. Sadhana, 25(5):489–510, 2000.
 R. Koo and S. Toueg. Checkpointing and rollback-recovery for distributed systems. IEEE Transactions on software Engineering, (1):23–31, 1987.
 D. Manivannan, R. H. B. Netzer, and M. Singhal. Finding consistent global checkpoints in a distributed computation. IEEE Transactions on Parallel and Distributed Systems, 8(6):623–627, 1997.
 D. Manivannan and M. Singhal. Quasi-synchronous checkpointing: Models, characterization, and classification. IEEE Transactions on Parallel and Distributed Systems, 10(7):703– 713, 1999.
 D. Manivannan and M. Singhal. Asynchronous recovery without using vector timestamps. Journal of Parallel and Distributed Computing, 62(12):1695–1728, 2002.
 C. M´etayer, J. Abrial, and L. Voisin. Event-b language, rodin deliverable d7. eu-project rodin (ist-511599)(2005), 2005.
 M. T. O¨ zsu and P. Valduriez. Principles of distributed database systems. Springer Science & Business Media, 2011.
 B. Randell. System structure for software fault tolerance. Ieee transactions on software engineering, (2):220–232, 1975.
 D. L. Russell. State restoration in systems of communicating processes. IEEE Transactions on Software Engineering, (2):183– 194, 1980.
Event-B, Formal Verification, Distributed systems, Recovery, Checkpoint, Formal Specifications, tentative checkpoint number, permanent checkpoint number, Formal Methods.