Functional Behavior of a Cardiac Pacing System

International audienceBuilding 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