Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Complete list of metadata
Contributor : Neeraj Kumar Singh Connect in order to contact the contributor
Submitted on : Friday, November 4, 2011 - 6:44:51 PM
Last modification on : Thursday, February 10, 2022 - 2:16:02 PM


  • HAL Id : inria-00638467, version 1



Dominique Méry, Neeraj Kumar Singh. EB2J : Code Generation from Event-B to Java. SBMF - Brazilian Symposium on Formal Methods, CBSoft - Brazilian Conference on Software: Theory and Practice, Sep 2011, São Paulo, Brazil. ⟨inria-00638467⟩



Record views