Where academic tradition
meets the exciting future

Code Generation and Scheduling of Event-B Models

Fredrik Degerlund, Richard Grönblom, Kaisa Sere, Code Generation and Scheduling of Event-B Models. TUCS Technical Reports 1027, Turku Centre for Computer Science, 2011.

Abstract:

Event-B is a formal method for full system modelling, and the RODIN
platform provides tool support for it. The method can be used for stepwise
development of parallel programs, but there are different approaches
to code generation and execution of the resulting code. In this paper, we demonstrate how C++ code can be generated using a separate plug-in for the RODIN
tool, and how the resulting code can be scheduled concurrently using
a dedicated tool. While our approach is related to animation in preserving
the event nature, it supports execution over several processors or a network
using the MPI (Message Passing Interface) framework.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tDeGrSe11a,
  title = {Code Generation and Scheduling of Event-B Models},
  author = {Degerlund, Fredrik and Grönblom, Richard and Sere, Kaisa},
  number = {1027},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2011},
  keywords = {Formal methods, Event-B, RODIN, scheduling, parallelism, MPI},
  ISBN = {978-952-12-2685-4},
}

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

Edit publication