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

Creating Sequential Programs from Event-B Models

Pontus Boström, Creating Sequential Programs from Event-B Models. In: Domique Méry, Stephan Merz (Eds.), Integrated Formal Methods: 8th International Conference (IFM2010), Lecture Notes in Computer Science 6396, 74–88, Springer, 2010.

Abstract:

Event-B is an emerging formal method with good tool support for various kinds of system modelling. However, the control flow in Event-B consists only of non-deterministic choice of enabled events. In many applications, notably in sequential program construction, more elaborate control flow mechanisms would be convenient. This paper explores a method, based on a scheduling language, for describing the flow of control. The aim is to be able to express schedules of events; to reason about their correctness; to create and verify patterns for introducing correct control flow. The conclusion is that using patterns, it is feasible to derive efficient sequential programs from event-based specifications in many cases.

BibTeX entry:

@INPROCEEDINGS{inpBostrom10a,
  title = {Creating Sequential Programs from Event-B Models},
  booktitle = {Integrated Formal Methods: 8th International Conference (IFM2010)},
  author = {Boström, Pontus},
  volume = {6396},
  series = {Lecture Notes in Computer Science},
  editor = {Méry, Domique and Merz, Stephan},
  publisher = {Springer},
  pages = {74–88},
  year = {2010},
}

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

Publication Forum rating of this publication: level 1

Edit publication