Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Pacemaker's Functional Behaviors in Event-B

Dominique Méry 1, * Neeraj Kumar Singh 1 
* Corresponding author
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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Neeraj Kumar Singh Connect in order to contact the contributor
Submitted on : Wednesday, September 30, 2009 - 4:09:24 PM
Last modification on : Thursday, October 27, 2022 - 4:02:56 AM
Long-term archiving on: : Saturday, November 26, 2016 - 11:57:30 AM


Files produced by the author(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⟩



Record views


Files downloads