Skip to Main content Skip to Navigation
Conference papers

Formal Development and Automatic Code Generation : Cardiac Pacemaker

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 : Formal methods are very efficient techniques for formal verification of a specification and to find errors in early stage of the system development. In order to generate a high quality code from a formal specification particularly in the embedded system is highly indispensable and a de-facto standard in many industrial application domains, such as medical, avionics and automotive control. This paper presents automatic source code generation from the developed formal specifications of a cardiac pacemaker. Cardiac pacing system is a Grand Challenge in the area of Software Verification. This paper includes an architecture of automatic code generation tool, summary of a formal development of the cardiac pacemaker using refinement techniques in Event-B, code generation of the developed formal model into C, C++, Java and C\# using code generation tool EB2ALL, and finally the code compilation and execution.
Complete list of metadatas
Contributor : Neeraj Kumar Singh <>
Submitted on : Friday, November 4, 2011 - 7:02:03 PM
Last modification on : Friday, September 4, 2020 - 11:20:25 AM


  • HAL Id : inria-00638486, version 1



Dominique Méry, Neeraj Kumar Singh. Formal Development and Automatic Code Generation : Cardiac Pacemaker. International Conference on Computers and Advanced Technology in Education (ICCATE, 2011), Nov 2011, Beijing, China. ⟨inria-00638486⟩



Record views