• 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. TUCS Technical Reports 955, Turku Centre for Computer Science, 2009.

Abstract:

Event-B is an emerging formal method with good tool support for various kinds of system modelling. However, efficient implementation of event based specifications created in Event-B as imperative programs has not been thoroughly explored. This paper explores methods to create efficient sequential code from Event-B models. The methods are based on a scheduling language for describing the flow of control in programs. The aim is to be able to express schedules of events, reasoning about their correctness and for creating and verifying implementation patterns. The conclusion is that using patterns, it is feasible to derive efficient sequential code from event based specifications in many cases. However, the extra proof obligations required in the process might sometimes make this approach infeasible.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tBostrom09a,
  title = {Creating Sequential Programs from Event-B Models},
  author = {Boström, Pontus},
  number = {955},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2009},
  keywords = {Event-B, Implementation, Sequential program development, Scheduling, Patterns },
  ISBN = {978-952-12-2338-9},
}

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

Edit publication