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.
Type de document :
Communication dans un congrès
International Conference on Computers and Advanced Technology in Education (ICCATE, 2011), Nov 2011, Beijing, China. 2011
Liste complète des métadonnées

https://hal.inria.fr/inria-00638486
Contributeur : Neeraj Kumar Singh <>
Soumis le : vendredi 4 novembre 2011 - 19:02:03
Dernière modification le : mardi 24 avril 2018 - 13:32:51

Identifiants

  • 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. 2011. 〈inria-00638486〉

Partager

Métriques

Consultations de la notice

306