Skip to Main content Skip to Navigation
New interface
Journal articles

Functional Behavior of a 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 : Building high quality and zero defects medical software-based devices is a critical task and formal modeling techniques can effectively help to achieve this target at certain level. Formal modeling of high-confidence Medical devices, such as those are too much error prone in operating, is an international Grand Challenge in the area of Verified Software. Modeling a pacemaker is one of the proposed challenge and we are considering the complete description of pacemaker's functionalities using an incremental proof-based approach. 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 add functional and timing properties to the abstract system-level specifications using some intermediate models. The properties express system architecture, action-reaction and timing behavior. This paper presents the formal model and refinement-based tree structure of all possible operating modes of the one- and two-electrode pacemaker that helps to develop consistent system with optimized code structure. Every stage of refinement includes detailed informations about the pacemaker operating modes. Models are expressed in the Event-B modeling language, which integrates conditions (called proof obligations) for checking their internal consistency with respect to invariants and safety properties and events. Generated proof obligations of models are proved by RODIN tool and desired behavior of the system is validated by the ProB tool according to the medical experts. ProB is an animator and model checker for the Event-B.
Document type :
Journal articles
Complete list of metadata
Contributor : Neeraj Kumar Singh Connect in order to contact the contributor
Submitted on : Thursday, November 25, 2010 - 7:26:03 PM
Last modification on : Thursday, February 10, 2022 - 2:16:02 PM


  • HAL Id : inria-00540007, version 1



Dominique Méry, Neeraj Kumar Singh. Functional Behavior of a Cardiac Pacing System. International Journal of Discrete Event Control Systems (IJDECS), 2010. ⟨inria-00540007⟩



Record views