Technical Report on Formal Development of Two-Electrode Cardiac Pacing System

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 build a high quality and zero defects medical devices and softwares is a crucial task. Formal modeling techniques help to achieve this target at certain level. Formal modeling of High-Confidence Medical devices those are too much error prone in operating, are an International Grand Challenge in the area of Verified Software. Formal modeling of an artificial pacemaker is also one of the proposed challenge. The architecture and functional behaviour of the double electrode pacemaker is more complex than the single electrode pacemaker. Proof-based an incremental approach, we use to develop the formal model of functional behaviour of the double electrode pacemaker. The incremental proof-based development is mainly driven by the refinement between an abstract model of the system and its detailed design through a series of refinements, which adds parametric based functional properties to the abstract system-level specifications using some intermediate models. The properties express system architecture and action-reaction under real-time constraints. This technical report focuses on the formal development of the double electrode operating modes and finds the common architecture of operating modes in tree form that helps to make the consistent system. The \eventb modeling language is used to express the double electrode pacemaker and generated proof obligations are proved by RODIN platform. Finally, the pacemaker model has been validated by an Event B animator ProB tool.
Type de document :
[Research Report] 2010
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger
Contributeur : Dominique Méry <>
Soumis le : mardi 13 avril 2010 - 16:59:14
Dernière modification le : mardi 24 avril 2018 - 13:35:59
Document(s) archivé(s) le : mercredi 30 novembre 2016 - 17:10:53


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00465061, version 2



Dominique Méry, Neeraj Kumar Singh. Technical Report on Formal Development of Two-Electrode Cardiac Pacing System. [Research Report] 2010. 〈inria-00465061v2〉



Consultations de la notice


Téléchargements de fichiers