Pacemaker's Functional Behaviors in Event-B

Dominique Méry 1, * Neeraj Kumar Singh 1
* Auteur correspondant
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Test and Simulation are the only verification techniques used for any biomedical devices such as pacemaker system, implantable cardioverter/defibrillators (ICDs) etc. The construction of formal models of Pacemaker systems is a considerable practical challenge. Formal modeling of an artificial Pacemaker system is a case study proposed by the software quality research laboratory at McMaster University in the Grand Challenge Initiative. Using an incremental proof-based approach, we model functionalities of the Pacemaker. The approach is illustrated by developing a new formal model of the cardiac pacemaker system. Our contribution are in this report to model the single electrode pacemaker system using Event-B and prove it. 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. A series of refinements is progressively added the functional and the timing properties to the abstract system-level specifications using some intermediate models. The properties express system architecture, action-reaction and timing behavior. This paper uses all possible operational modes of a single electrode Pacemaker system that helps to develop better hardware. Every stage of refinement includes the detail information about operating modes. The models are expressed in Event-B modeling language and validated primarily by the ProB tool in different situation such as hysteresis and rate adapting pacing under real-time constraints. In each stages of refinements include the detail information and more events are introduced. The final step of refinement completely localized the events and similar to implementation of single electrode pacemaker operating modes system. The stepwise refinement of the single electrode Pacemaker system contributes to achieve a high degree of automatic proof.
Type de document :
[Research Report] 2009
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger
Contributeur : Neeraj Kumar Singh <>
Soumis le : mercredi 30 septembre 2009 - 16:09:24
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : samedi 26 novembre 2016 - 11:57:30


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


  • HAL Id : inria-00419973, version 2



Dominique Méry, Neeraj Kumar Singh. Pacemaker's Functional Behaviors in Event-B. [Research Report] 2009. 〈inria-00419973v2〉



Consultations de la notice


Téléchargements de fichiers