Skip to main content
SpringerLink
Log in
Book cover

Data, Engineering and Applications pp 229–241Cite as

Formal Verification of Causal Order-Based Load Distribution Mechanism Using Event-B

  • Chapter
  • First Online:

Abstract

Formal methods are mathematical techniques that use the concepts and ideas from mathematics and formal logic to specify and reason about system properties. It provides a framework which makes it possible to write specification, analyse and verify the model in a systematic way. Event-B is a formal method which is used to develop and verify the model of distributed systems. Event-B follows refinement-based approach to develop a complex model. In this paper, we have formally verified distributed load migration from heavily loaded site to low load site using Event-B. In order to provide fairness to load transfer mechanism, we have introduced a notion of causal order. The request for load transfer of that site will be completed first whose load request message causally precedes load request messages of other sites.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   139.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Bjrner, D.: Logics of formal specification languages. Comput. Inform. 22(1–2), This double issue contains the following papers on B, CafeOBJ, CASL, RAISE, TLA+ and Z (2003)

    Google Scholar 

  2. Bjrner, D.: Special double issue on formal methods of program development. Int. J. Softw. Inform. 3 (2009)

    Google Scholar 

  3. Shankar, N.: Combining theorem proving and model checking through symbolic analysis. In: Proceeding of CONCUR ’00, vol. 1877, pp. 1–16. LNCS, Springer (2000)

    Google Scholar 

  4. Fitzgerald, J., Larsen, P.G.: Modelling Systems—Practical Tools and Techniques in Software Development. Cambridge University Press, Cambridge, UK, Second edition (2009)

    MATH  Google Scholar 

  5. Clarke, E., Zhao, X.: A theorem prover for mathematica. In automated deduction-CADE-II. In: 11th International Conference on Automated Deduction, pp. 761–763. Saratoga Springs, New York, 15–18 June 1992

    Google Scholar 

  6. Clarke, E., Zhao, X.: A theorem prover for Mathematica. Math. J. (1993)

    Google Scholar 

  7. Abrial, J., Butler,M., Hallerstede,S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM, Lecture Notes in Computer Science, vol. 4260, pp. 588–605. Springer (2006)

    Google Scholar 

  8. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. CambridgeUniversity Press (2010)

    Google Scholar 

  9. Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models. Appl. Event B Fundam. Inform. 77(1–2), 1–28 (2007)

    Google Scholar 

  10. Butler, M.: An approach to the design of distributed systems with B AMN. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM, Lecture Notes in Computer Science, vol. 1212, pp. 223–241. Springer (1997)

    Google Scholar 

  11. Singhal, M., Shivratri, N.G.: Advanced Concepts in Operating Systems. Tata McGraw-Hill Book Company (2012)

    Google Scholar 

  12. Lazowska, D.E., Zahorjan, J.: Adaptive load sharing in homogeneous distributed systems. IEEE Trans. Softw. Eng. 12(5), 662–675 (1986)

    Google Scholar 

  13. Lazowska, D.E., Zahorjan, J.: A Comparison of receiver-initiated and sender-initiated adaptive load sharing. Perform. Eval. 6(1) 53–68 (1986)

    Google Scholar 

  14. Yadav, D., Butler, M.: Application of Event B to global causal ordering for fault tolerant transactions. In: Proceeding of Workshop on Rigorous Engineering of Fault Tolerant System, REFT05, Newcastle upon Tyne, pp. 93–103, 19 July 2005

    Google Scholar 

  15. Yadav, D., Butler, M.: Rigorous design of fault-tolerant transactions for replicated database systems using Event B. In: Butler, M., Jones, C.B., Romanovsky, A, Troubitsyna, E. (eds.) Rigorous Development of Complex Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 4157, pp. 343–363. Springer, Heidelberg (2006)

    Google Scholar 

  16. Yeganefard, S., Butler, M., Rezazadeh, A.: Evaluation of a guideline by formal modelling of cruise control system in Event-B. Proc. NFM 2010, 182–191 (2010)

    Google Scholar 

  17. Liu, J., Liu, J.: A formal framework for hybrid Event B. Electron. Notes Theor. Sci. 309(2014), 3–12 (2014) (Elsevier)

    Google Scholar 

  18. Suryavanshi, R., Yadav, D.: Formal development of byzantine immune total order broadcast system using Event-B. In: Andres, F., Kannan, R. (eds.) ICDEM 2010. LNCS, vol. 6411, pp. 317–324. Springer, Germany (2010)

    Google Scholar 

  19. Hallerstede, S., Leuschel, M.: Experiments in program verification using Event-B. Form. Asp. Comput. 24, 97–125 (2012)

    MathSciNet  MATH  Google Scholar 

  20. Suryavanshi, R., Yadav, D.: Rigorous design of lazy replication system using Event-B. In: Communications in Computer and Information Science, vol. 0306, pp. 400–411. Springer, Germany (2012). ISSN 1865-0929

    Google Scholar 

  21. Suryavanshi, R., Yadav, D.: Modeling of multiversion concurrency control system using Event-B. In: Federated Conference on Computer Science and Information systems (FedCSIS), Poland, indexed and published by IEEE, pp. 1397–1401, 9–12 Sept 2012. ISBN 978-83-60810-51-4

    Google Scholar 

  22. Banach, R.: Retrenchment for Event-B: usecase-wise development and Rodin integration. Form. Asp. Comput. 23, 113–131 (2011)

    MATH  Google Scholar 

  23. Abrial, J.R., Cansell, D., Mery, D.: A mechanically proved and incremental development of ieee 1394 tree identify protocol. Form. Asp. Comput. 14(3), 215–227 (2003)

    MATH  Google Scholar 

  24. Metayer, C., Abrial,J.R., Voison, L.: Event-B language. RODIN deliverables 3.2. http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf (2005)

  25. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 25(7), 558–565 (1978)

    MATH  Google Scholar 

  26. Birman, K., Schiper, A., Stephenson, P.: Lightweight causal and atomic group multicast. ACM Trans. Comput. Syst. 9(3), 272–314 (1991)

    Google Scholar 

  27. Yadav, D., Butler, M.: Formal specifications and verification of message ordering properties in a broadcast system using Event B. In: Technical Report, School of Electronics and Computer Science, University of Southampton, Southampton, UK (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Abdul Kalam Technical University, Lucknow, 226031, India

    Pooja Yadav

  2. Pranveer Singh Institute of Technology, Kanpur, 209305, India

    Raghuraj Suryavanshi

  3. Rajkiya Engineering College, Kannauj, 209732, India

    Arun Kumar Singh

  4. Institute of Engineering and Technology, Lucknow, 226021, India

    Divakar Yadav

Authors
  1. Pooja Yadav
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Raghuraj Suryavanshi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Arun Kumar Singh
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Divakar Yadav
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Raghuraj Suryavanshi .

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Sagar Institute of Research & Technology (SIRT), Bhopal, Madhya Pradesh, India

    Rajesh Kumar Shukla

  2. School of Information Technology, Rajiv Gandhi Technical University, Bhopal, Madhya Pradesh, India

    Jitendra Agrawal

  3. School of Information Technology, Rajiv Gandhi Technological University, Bhopal, Madhya Pradesh, India

    Sanjeev Sharma

  4. THDC Institute of Hydropower Engineering and Technology, Tehri, Uttarakhand, India

    Geetam Singh Tomer

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Singapore Pte Ltd.

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Yadav, P., Suryavanshi, R., Singh, A.K., Yadav, D. (2019). Formal Verification of Causal Order-Based Load Distribution Mechanism Using Event-B. In: Shukla, R.K., Agrawal, J., Sharma, S., Singh Tomer, G. (eds) Data, Engineering and Applications. Springer, Singapore. https://doi.org/10.1007/978-981-13-6351-1_18

Download citation

  • DOI: https://doi.org/10.1007/978-981-13-6351-1_18

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-13-6350-4

  • Online ISBN: 978-981-13-6351-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation