Concurrent Scheduling of Event-B Models

Pontus Boström
Fredrik Degerlund
Kaisa Sere
Marina Waldén

Event-B is a refinement-based formal method that has been shown to be useful in developing concurrent and distributed programs. Large 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. We explore how schedules can be designed so that their application results in a correctness-preserving refinement step. For practical application, two patterns for schedule introduction are provided, together with their associated proof obligations. We demonstrate our method by applying it on the dining philosophers problem.

In John Derrick, Eerke Boiten and Steve Reeves: Proceedings 15th International Refinement Workshop (Refine 2011), Limerick, Ireland, 20th June 2011, Electronic Proceedings in Theoretical Computer Science 55, pp. 166–182.
Published: 17th June 2011.

ArXived at: https://dx.doi.org/10.4204/EPTCS.55.11 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org