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.
Complete list of metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/inria-00465061
Contributor : Dominique Méry <>
Submitted on : Tuesday, April 13, 2010 - 4:59:14 PM
Last modification on : Thursday, September 19, 2019 - 5:00:04 PM
Long-term archiving on : Wednesday, November 30, 2016 - 5:10:53 PM

File

Report_2electrode.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00465061, version 2

Collections

Citation

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

Share

Metrics

Record views

556

Files downloads

755