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

https://hal.inria.fr/inria-00638486
Contributor : Neeraj Kumar Singh <>
Submitted on : Friday, November 4, 2011 - 7:02:03 PM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM

Identifiers

  • HAL Id : inria-00638486, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

351