Advertisement

Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Derivation of concurrent programs by stepwise scheduling of Event-B models

Abstract

Concurrent programs are often complex and they are not straightforward to develop and prove correct. Formal development methods based on refinement make it possible not only to derive programs gradually, but also to prove their correctness in a stepwise fashion. Event-B is a formal framework that has been shown useful for developing concurrent and distributed programs. In order to scale to large systems, models can be decomposed into sub-models that can be refined semi-independently and executed in parallel. In this paper, we show how to introduce explicit control flow for the concurrent sub-models in the form of event schedules. The purpose of these schedules is both to provide process-oriented specifications of the programs to complement the state-based approach in Event-B, as well as to facilitate more efficient implementation of the models. The schedules are introduced in a stepwise manner and should be designed to result in a correctness-preserving refinement step. In order to reduce the verification burden on the developers, we provide patterns for schedule introduction, together with their associated proof obligations. We demonstrate our method by applying it on the dining philosophers problem.

This is a preview of subscription content, log in to check access.

References

  1. Abr10

    Abrial J-R (2010) Modeling in Event B: system and software engineering. Cambridge University Press, Cambridge

  2. AH07

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

  3. BDSW11

    Boström P, Degerlund F, Sere K, Waldén M (2011) Concurrent scheduling of Event-B models. In: Proceedings 15th international refinement workshop, pp 166–182. http://dx.doi.org/10.4204/EPTCS.55.11

  4. BE11

    Butler M, Edmunds A (2011) Tasking Event-B: an extension to Event-B for generating concurrent code. In: PLACES 2011 workshop, 2011.http://places11.di.fc.ul.pt/proceedings.pdf/view

  5. BKS83

    Back R-JR, Kurki-Suonio R (1983) Decentralization of process nets with centralized control. In: Proceedings of the 2nd ACM SIGACT-SIGOPS symposium of principles of distributed computing, pp 131–142

  6. Bos10

    Boström P (2010) Creating sequential programs from Event-B models. In: IFM’10 Proceedings of the 8th international conference on integrated formal methods, volume 6396 of LNCS. Springer, New York, pp 74–88

  7. BS91

    Back R-JR, Sere K (1991) Stepwise refinement of action systems. Struct Program 12: 17–30

  8. But00

    Butler M (2000) csp2B: a practical approach to combining CSP and B. Formal Aspects Comput 12(3): 182–198

  9. BvW90

    Back R, von Wright J (1990) Refinement calculus, part I: sequential nondeterministic programs. In: de Bakker J, de Roever W, Rozenberg G (eds) Stepwise refinement of distributed systems models, formalisms, correctness, volume 430 of Lecture Notes in Computer Science. Springer, Berlin, pp 42–66

  10. BvW98

    Back R-JR, von Wright J (1998) Refinement calculus: a systematic introduction. Graduate Texts in Computer Science. Springer, Berlin

  11. BvW99

    Back R-JR, von Wright J (1999) Reasoning algebraically about loops. Acta Inform 36: 295–334

  12. BvW03

    Back R-JR, von Wright J (2003) Compositional action system refinement. Formal Aspects Comput 15: 103–117

  13. CSW03

    Cavalcanti A, Sampaio A, Woodcock J (2003) A refinement strategy for circus. Formal Aspects Comput 15: 146–181

  14. DGS11

    Degerlund F, Grönblom R, Sere K (2011) Code generation and scheduling of Event-B models. Technical Report 1027. Turku Centre for Computer Science (TUCS)

  15. Edm10

    Edmunds A (2010) Providing concurrent implementations for Event-B developments. PhD thesis, University of Southampton, School of Electronics and Computer Science

  16. Gro09

    Grönblom R (2009) A framework for code generation and parallel execution of Event-B models. Master’s thesis, Åbo Akademi University

  17. HA10

    Hoang TS, Abrial J-R (2010) Event-B decomposition for parallel programs. In: Abstract state machines, B and Z, volume 5977 of LNCS. Springer, Berlin, pp 319–333

  18. Hal08

    Hallerstede S (2008) On the purpose of Event-B proof obligations. In: Abstract state machines, B and Z, volume 5238 of LNCS. Springer, Berlin, pp 125–138

  19. Hal10

    Hallerstede S (2010) Structured Event-B models and proofs. In: Abstract state machines, B and Z, volume 5977 of LNCS. Springer, Berlin, pp 273–286

  20. Hoa78

    Hoare CAR (1978) Communicating sequential processes. Commun ACM 21: 666–677

  21. Hoa85

    Hoare CAR (1985) Communicating sequential processes. Prentice Hall, Upper Saddle River

  22. Ili09

    Iliasov A (2009) On Event-B and control flow. Technical Report CS-TR-1159. School of Computing Science, Newcastle University

  23. Jon83

    Jones CB (1983) Tentative steps toward a development method for interfering programs. Trans Program Lang Syst 5(4): 596–619

  24. MS10

    Méry D, Singh NK (2010) EB2C: a tool for Event-B to C conversion support. In: Poster and tool demo presentation at SEFM 2010.http://hal.inria.fr/inria-00540006/PDF/cameraready-sefm2010.pdf

  25. OG76

    Owicki SS, Gries D (1976) An axiomatic proof technique for parallel programs I. Acta Inform 6: 319–340

  26. PSW05

    Plosila J, Sere K, Waldén M (2005) Asynchronous system synthesis. Sci Comput Program 55: 259–288

  27. Rod

    Rodin platform.http://www.event-b.org

  28. Roe01

    de Roever WP et al (2001) Concurrency Verification: Introduction to compositional and noncompositional methods. Cambridge University Press, Cambridge

  29. SS96

    Sekerinski E, Sere K (1996) A theory of prioritizing composition. Comput J 39(8): 701–712

  30. STW10

    Schneider S, Treharne H, Wehrheim H (2010) A CSP approach to control in Event-B. In: Integrated formal methods 2010, volume 6396 of LNCS. Springer, Berlin, pp 260–274

  31. Wri09

    Wright S (2009) Automatic generation of C from Event-B. In: Workshop on integration of model-based formal methods and tools.http://www.cs.bris.ac.uk/Publications/pub_master.jsp?id=2000990

Download references

Author information

Correspondence to Fredrik Degerlund.

Additional information

Eerke Boiten, John Derrick and Steve Reeves

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Boström, P., Degerlund, F., Sere, K. et al. Derivation of concurrent programs by stepwise scheduling of Event-B models. Form Asp Comp 26, 281–303 (2014). https://doi.org/10.1007/s00165-012-0260-5

Download citation

Keywords

  • Concurrency
  • Event-B
  • Patterns
  • Scheduling
  • Stepwise development