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.
Type de document :
Article dans une revue
International Journal of Discrete Event Control Systems (IJDECS), Dr. Mohamed Khalgui, 2010
Liste complète des métadonnées
Contributeur : Neeraj Kumar Singh <>
Soumis le : jeudi 25 novembre 2010 - 19:26:03
Dernière modification le : mardi 24 avril 2018 - 13:32:55


  • 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), Dr. Mohamed Khalgui, 2010. 〈inria-00540007〉



Consultations de la notice