Top

Published in:

2019 | OriginalPaper | Chapter

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

Authors : Pooja Yadav, Raghuraj Suryavanshi, Arun Kumar Singh, Divakar Yadav

Published in: Data, Engineering and Applications

Publisher: Springer Singapore

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Enhanced and Secure Acknowledgement IDS in Mobile Ad Hoc Network by Hybrid Cryptography Technique

next chapter An IOT-Based Architecture for Crime Management in Nigeria

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)

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

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

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

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

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

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)

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

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

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)

11.

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

12.

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

13.

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

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

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)

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)

17.

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

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)

19.

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

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

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

22.

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

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

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

26.

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

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)

Title: Formal Verification of Causal Order-Based Load Distribution Mechanism Using Event-B
Authors: Pooja Yadav
Raghuraj Suryavanshi
Arun Kumar Singh
Divakar Yadav
Publisher: Springer Singapore
Book: Data, Engineering and Applications
Print ISBN: 978-981-13-6350-4

Electronic ISBN: 978-981-13-6351-1

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-981-13-6351-1_18

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner