EB2J : Code Generation from Event-B to Java

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 : To use formal methods effectively in the object-oriented based development process, it is highly desirable that the formal specification be translated to Java code, a de facto standard in many industrial critical application domains, such as medical, avionics and automotive control, where the developed system is dynamically bound on multiple hardware platforms with correct runtime support. This goal can be achieved by developing a proof-based formal model and automatic generation of source code from the formal model. The generated source code must be ensured that the produced code behavior is complied with formal specification abstractly. In this context we have developed EB2J, a software tool that translates Event-B models into Java code. This paper discusses the code generation approach underlying EB2J tool. The effectiveness of EB2J is illustrated through automatic generation of a Java code from the formal specification of a cardiac pacemaker.
Type de document :
Communication dans un congrès
SBMF - Brazilian Symposium on Formal Methods, Sep 2011, São Paulo, Brazil. 2011
Liste complète des métadonnées

https://hal.inria.fr/inria-00638467
Contributeur : Neeraj Kumar Singh <>
Soumis le : vendredi 4 novembre 2011 - 18:44:51
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Identifiants

  • HAL Id : inria-00638467, version 1

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. EB2J : Code Generation from Event-B to Java. SBMF - Brazilian Symposium on Formal Methods, Sep 2011, São Paulo, Brazil. 2011. 〈inria-00638467〉

Partager

Métriques

Consultations de la notice

318