×

zbMATH — the first resource for mathematics

Derivation of concurrent programs by stepwise scheduling of Event-B models. (English) Zbl 1342.68056
Summary: 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.

MSC:
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Circus; csp2B; Rodin
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrial J-R (2010) Modeling in Event B: system and software engineering. Cambridge University Press, Cambridge · Zbl 1213.68214
[2] Abrial, J-R; Hallerstede, S, Refinement, decomposition, and instantiation of discrete models: application to event-B, Fundam Inform, 77, 1-28, (2007) · Zbl 1118.68392
[3] 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 · Zbl 0517.68032
[4] 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 · Zbl 1118.68392
[5] 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 · Zbl 0383.68028
[6] 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] Back, R-JR; Sere, K, Stepwise refinement of action systems, Struct Program, 12, 17-30, (1991)
[8] Butler, M, Csp2B: a practical approach to combining CSP and B, Formal Aspects Comput, 12, 182-198, (2000) · Zbl 0969.68578
[9] 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] Back R-JR, von Wright J (1998) Refinement calculus: a systematic introduction. Graduate Texts in Computer Science. Springer, Berlin · Zbl 0949.68094
[11] Back, R-JR; Wright, J, Reasoning algebraically about loops, Acta Inform, 36, 295-334, (1999) · Zbl 0940.68011
[12] Back, R-JR; Wright, J, Compositional action system refinement, Formal Aspects Comput, 15, 103-117, (2003) · Zbl 1093.68007
[13] Cavalcanti, A; Sampaio, A; Woodcock, J, A refinement strategy for circus, Formal Aspects Comput, 15, 146-181, (2003) · Zbl 1093.68555
[14] 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) · Zbl 0969.68578
[15] Edmunds A (2010) Providing concurrent implementations for Event-B developments. PhD thesis, University of Southampton, School of Electronics and Computer Science · Zbl 1075.68618
[16] Grönblom R (2009) A framework for code generation and parallel execution of Event-B models. Master’s thesis, Åbo Akademi University
[17] 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] 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 · Zbl 1156.68348
[19] 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] Hoare, CAR, Communicating sequential processes, Commun ACM, 21, 666-677, (1978) · Zbl 0383.68028
[21] Hoare CAR (1985) Communicating sequential processes. Prentice Hall, Upper Saddle River · Zbl 0637.68007
[22] Iliasov A (2009) On Event-B and control flow. Technical Report CS-TR-1159. School of Computing Science, Newcastle University
[23] Jones, CB, Tentative steps toward a development method for interfering programs, Trans Program Lang Syst, 5, 596-619, (1983) · Zbl 0517.68032
[24] 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] Owicki, SS; Gries, D, An axiomatic proof technique for parallel programs I, Acta Inform, 6, 319-340, (1976) · Zbl 0312.68011
[26] Plosila, J; Sere, K; Waldén, M, Asynchronous system synthesis, Sci Comput Program, 55, 259-288, (2005) · Zbl 1075.68618
[27] Rodin platform.http://www.event-b.org
[28] de Roever WP et al (2001) Concurrency Verification: Introduction to compositional and noncompositional methods. Cambridge University Press, Cambridge · Zbl 1009.68020
[29] Sekerinski, E; Sere, K, A theory of prioritizing composition, Comput J, 39, 701-712, (1996)
[30] 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] 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 · Zbl 0517.68032
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.