Technical Report on Formal Development of Two-Electrode Cardiac Pacing System

To build a high quality and zero defects medical devices and softwares is a crucial task. Formal modeling techniques help to achieve this target at certain level. Formal modeling of High-Confidence Medical devices those are too much error prone in operating, are an International Grand Challenge in the area of Verified Software. Formal modeling of an artificial pacemaker is also one of the proposed challenge. The architecture and functional behaviour of the double electrode pacemaker is more complex than the single electrode pacemaker. Proof-based an incremental approach, we use to develop the formal model of functional behaviour of the double electrode pacemaker. 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 adds parametric based functional properties to the abstract system-level specifications using some intermediate models. The properties express system architecture and action-reaction under real-time constraints. This technical report focuses on the formal development of the double electrode operating modes and finds the common architecture of operating modes in tree form that helps to make the consistent system. The \eventb modeling language is used to express the double electrode pacemaker and generated proof obligations are proved by RODIN platform. Finally, the pacemaker model has been validated by an Event B animator ProB tool