Where academic tradition
meets the exciting future

Derivation of Structural VHDL from Component-Based Event-B Models

Sergey Ostroumov, Leonidas Tsiopoulos, Juha Plosila, Kaisa Sere, Derivation of Structural VHDL from Component-Based Event-B Models. In: Michael Butler, Stefan Hallerstede, Marina Walden (Eds.), Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes 18, 31–32, TUCS, 2013.

Abstract:

We propose an approach to integrating formal modeling and verification with hardware code generation. The former allows a designer to reduce error cost due to its strong mathematical background and application at the earliest design phases. The latter contributes to the derivation of an implementation in an automated manner. We utilize Event-B as the formal framework. It facilitates formalization and verification of complex systems by stepwise unfolding of system properties. Furthermore, Event-B has mature tool support – the Rodin platform. We develop a plug-in for this platform that allows designers to generate a structural, i.e., component-based, VHDL description from formal models.

BibTeX entry:

@INPROCEEDINGS{inpOsTsPlSe13b,
  title = {Derivation of Structural VHDL from Component-Based Event-B Models},
  booktitle = {Proceedings of the 4th Rodin User and Developer Workshop},
  author = {Ostroumov, Sergey and Tsiopoulos, Leonidas and Plosila, Juha and Sere, Kaisa},
  volume = {18},
  series = {TUCS Lecture Notes},
  editor = {Butler, Michael and Hallerstede, Stefan and Walden, Marina},
  publisher = {TUCS},
  pages = {31–32},
  year = {2013},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab), Embedded Systems Laboratory (ESLAB), Embedded Computer and Electronic Systems (ECES)

Edit publication