• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Concurrent Scheduling of Event-B Models

Pontus Boström, Fredrik Degerlund, Kaisa Sere, Marina Waldén, Concurrent Scheduling of Event-B Models. In: John Derrick, Eerke A. Boiten, Steve Reeves (Eds.), Proceedings 15th International Refinement Workshop, Electronic Proceedings in Theoretical Computer Science 55, 166–182, Open Publishing Association, 2011.

http://dx.doi.org/10.4204/EPTCS.55.11

Abstract:

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.

BibTeX entry:

@INPROCEEDINGS{iBoDeSeWa11a,
  title = {Concurrent Scheduling of Event-B Models},
  booktitle = {Proceedings 15th International Refinement Workshop},
  author = {Boström, Pontus and Degerlund, Fredrik and Sere, Kaisa and Waldén, Marina},
  volume = {55},
  series = {Electronic Proceedings in Theoretical Computer Science},
  editor = {Derrick, John and Boiten, Eerke A. and Reeves, Steve},
  publisher = {Open Publishing Association},
  pages = {166–182},
  year = {2011},
  keywords = {Concurrency, Event-B, Patterns, Scheduling},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication