Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Generation of Structural VHDL ...

Generation of Structural VHDL Code with Library Components from Formal Event-B Models

Sergey Ostroumov, Leonidas Tsiopoulos, Juha Plosila, Kaisa Sere, Generation of Structural VHDL Code with Library Components from Formal Event-B Models. TUCS Technical Reports 1073, TUCS, 2013.

Abstract:

We propose a design approach to integrating correct-by-construction formal modeling with hardware implementations in VHDL. Formal modeling is performed within the Event-B framework that supports the refinement approach, i.e., stepwise unfolding of system properties in a correct-by-construction manner. After an implementable deterministic model of a hardware system is derived, we apply an additional refinement step in order to introduce hardware library components in the form of functions. We show the mapping between these functions and corresponding library components such that a structural, i.e., component-based, VHDL description is derived. The application of functions binds unrestricted data types and substitutes regular operations with function calls. The approach is presented through examples that illustrate the additional refinement step and the code generation. We show the advantages in terms of occupied area and performance of the descriptions that incorporate hardware library components. In addition, we show generation of test cases from a formal model, which facilitates conformance or online testing.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tOsTsPlSe13a,
  title = {Generation of Structural VHDL Code with Library Components from Formal Event-B Models},
  author = {Ostroumov, Sergey and Tsiopoulos, Leonidas and Plosila, Juha and Sere, Kaisa},
  number = {1073},
  series = {TUCS Technical Reports},
  publisher = {TUCS},
  year = {2013},
  keywords = {automated refinement, code generation, design flow, Event-B, formal methods, library components, structural VHDL, test cases generation},
  ISBN = {978-952-12-2869-8},
}

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

Edit publication