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

Technical Report on Formal Development of Two-Electrode 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 : 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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [33 references]  Display  Hide  Download
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Tuesday, April 13, 2010 - 4:59:14 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:37 AM
Long-term archiving on: : Wednesday, November 30, 2016 - 5:10:53 PM


Files produced by the author(s)


  • HAL Id : inria-00465061, version 2



Dominique Méry, Neeraj Kumar Singh. Technical Report on Formal Development of Two-Electrode Cardiac Pacing System. [Research Report] 2010. ⟨inria-00465061v2⟩



Record views


Files downloads