Automatic Code Generation from Event-B Models

Dominique Méry 1 Neeraj Kumar Singh 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents a translation tool that automatically generates efficient target programming language code (C, C++, Java and C#) from Event-B formal specification related to the analysis of complex problems. This tool is a collection of plug-ins, which are used for translating Event-B formal specifications into different kinds of programming languages. The translation tool is rigorously developed with safety properties preservation. The results detailed in this paper are an architecture of the translation process, to generate a target language code from Event-B models using Event-B grammar through syntax-directed translation, code scheduling architecture and verification of an automatic generated code. The translator checks syntax and type consistency before generating the target programming language code. The translation tool has been developed as a set of Rodin plug-ins under the Eclipse development framework. An assessment of the proposed approach is given through a case study, relative to the development of a cardiac pacemaker system.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00637765
Contributor : Neeraj Kumar Singh <>
Submitted on : Wednesday, November 2, 2011 - 6:37:19 PM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM

Identifiers

  • HAL Id : inria-00637765, version 1

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. Automatic Code Generation from Event-B Models. SoICT 2011, Hanoi University, Oct 2011, Hanoi, Vietnam. ⟨inria-00637765⟩

Share

Metrics

Record views

297