Automatic Code Generation from Event-B Models - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

Automatic Code Generation from Event-B Models

(1) , (1)
1

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.
Not file

Dates and versions

inria-00637765 , version 1 (02-11-2011)

Identifiers

  • HAL Id : inria-00637765 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More