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

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

  IJETT-book-cover  International Journal of Engineering Trends and Technology (IJETT)          
  
© 2021 by IJETT Journal
Volume-69 Issue-4
Year of Publication : 2021
Authors : Bal Krishna Saraswat, Raghuraj Suryavanshi, Divakar Yadav
DOI :  10.14445/22315381/IJETT-V69I4P201

Citation 

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.

Abstract
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.

Reference
[1] J. Abrial. The b-book: assigning programs to meanings cambridge university press, 1996.
[2] J.-R. Abrial. Extending b without changing it (for developing distributed systems). In 1st Conference on the B method, volume 11, 1996.
[3] 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.
[4] J.-R. Abrial and J.-R. Abrial. The B-book: assigning programs to meanings. Cambridge University Press, 2005.
[5] 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.
[6] 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.
[7] 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.
[8] 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.
[9] R. Banach. Retrenchment for event-b: Usecase-wise development and rodin integration. Formal Aspects of Computing, 23(1):113– 131, 2011.
[10] 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.
[11] J.-L. Boulanger. Formal methods applied to complex systems: implementation of the B method. John Wiley & Sons, 2014.
[12] M. Butler and D. Yadav. An incremental development of the mondex system in event-b. Formal Aspects of Computing, 20(1):61–77, 2008.
[13] 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.
[14] Clearsy. B4free tool homepage. www.b4free.com.
[15] 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.
[16] S. Hallerstede. Justifications for the event-b modelling notation. In International Conference of B Users, pages 49–63. Springer, 2007.
[17] 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.
[18] S. Kalaiselvi and V. Rajaraman. A survey of checkpointing algorithms for parallel and distributed computers. Sadhana, 25(5):489–510, 2000.
[19] R. Koo and S. Toueg. Checkpointing and rollback-recovery for distributed systems. IEEE Transactions on software Engineering, (1):23–31, 1987.
[20] 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.
[21] D. Manivannan and M. Singhal. Quasi-synchronous checkpointing: Models, characterization, and classification. IEEE Transactions on Parallel and Distributed Systems, 10(7):703– 713, 1999.
[22] D. Manivannan and M. Singhal. Asynchronous recovery without using vector timestamps. Journal of Parallel and Distributed Computing, 62(12):1695–1728, 2002.
[23] C. M´etayer, J. Abrial, and L. Voisin. Event-b language, rodin deliverable d7. eu-project rodin (ist-511599)(2005), 2005.
[24] M. T. O¨ zsu and P. Valduriez. Principles of distributed database systems. Springer Science & Business Media, 2011.
[25] B. Randell. System structure for software fault tolerance. Ieee transactions on software engineering, (2):220–232, 1975.
[26] D. L. Russell. State restoration in systems of communicating processes. IEEE Transactions on Software Engineering, (2):183– 194, 1980.

Keywords
Event-B, Formal Verification, Distributed systems, Recovery, Checkpoint, Formal Specifications, tentative checkpoint number, permanent checkpoint number, Formal Methods.