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.
Type de document :
Communication dans un congrès
SoICT 2011, Oct 2011, Hanoi, Vietnam. ACM ICPS, 2011
Liste complète des métadonnées

https://hal.inria.fr/inria-00637765
Contributeur : Neeraj Kumar Singh <>
Soumis le : mercredi 2 novembre 2011 - 18:37:19
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Identifiants

  • HAL Id : inria-00637765, version 1

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. Automatic Code Generation from Event-B Models. SoICT 2011, Oct 2011, Hanoi, Vietnam. ACM ICPS, 2011. 〈inria-00637765〉

Partager

Métriques

Consultations de la notice

220