Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > VHDL Code Generation from Form...

VHDL Code Generation from Formal Event-B Models

Sergey Ostroumov, Leonidas Tsiopoulos, VHDL Code Generation from Formal Event-B Models. In: Paris Kitsos (Ed.), Digital System Design: Architectures, Methods and Tools, 127–134, IEEE Computer Society Conference Publishing Services (CPS), 2011.

Abstract:

In this paper, we present an approach that allows to generate VHDL code from formal models developed with the Event-B formalism. The approach is based on the relationship between the structure of the formal model and hardware description language statements. We are aiming at getting VHDL code whose behaviour is the same as the behaviour of the Event-B model. Our contribution lies in the fact that we show the main similarity between the formal model and VHDL code that allows us to derive the method and, hence, the algorithm for automatic translation. This algorithm can be implemented as a plug-in for the Rodin tool which supports the Event-B formalism. The approach is presented through a simplified version of an industrial case study developed in a stepwise refinement manner. We also present several ways of possible translation depending on the way the model has been developed through refinement. In addition, we present synthesis results that show space occupied by the VHDL code generated.

BibTeX entry:

@INPROCEEDINGS{iOsTs11a,
  title = {VHDL Code Generation from Formal Event-B Models},
  booktitle = {Digital System Design: Architectures, Methods and Tools},
  author = {Ostroumov, Sergey and Tsiopoulos, Leonidas},
  editor = {Kitsos, Paris},
  publisher = {IEEE Computer Society Conference Publishing Services (CPS)},
  pages = {127–134},
  year = {2011},
  keywords = {formal  modelling; Event-B; VHDL; code generation},
}

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

Publication Forum rating of this publication: level 1

Edit publication