Academic
Publications
VHDL Code Generation from Formal Event-B Models

VHDL Code Generation from Formal Event-B Models,10.1109/DSD.2011.20,Sergey Ostroumov,Leonidas Tsiopoulos

VHDL Code Generation from Formal Event-B Models  
BibTex | RIS | RefWorks Download
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. Keywords-formal modelling; Event-B; VHDL; code generation
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.