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

Derivation of Concurrent Programs by Stepwise Scheduling of Event-B Models

Pontus Boström, Fredrik Degerlund, Kaisa Sere, Marina Waldén, Derivation of Concurrent Programs by Stepwise Scheduling of Event-B Models. Formal Aspects of Computing 26(2), 281–303, 2014.

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.

BibTeX entry:

@ARTICLE{jBoDeSeWa14a,
  title = {Derivation of Concurrent Programs by Stepwise Scheduling of Event-B Models},
  author = {Boström, Pontus and Degerlund, Fredrik and Sere, Kaisa and Waldén, Marina},
  journal = {Formal Aspects of Computing},
  volume = {26},
  number = {2},
  publisher = {Springer},
  pages = {281–303},
  year = {2014},
  ISSN = {0934-5043},
}

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

Publication Forum rating of this publication: level 2

Edit publication