OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Formalizing the Cardiac Pacemaker Resynchronization Therapy

Singh, Neeraj Kumar and Lawford, Mark and Maibaum, Thomas S. E. and Wassyng, Alan Formalizing the Cardiac Pacemaker Resynchronization Therapy. (2015) In: Digital Human Modeling - Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health - 6th International Conference (DHM 2015), 2 August 2015 - 7 August 2015 (Los Angeles, United States).

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
362kB

Official URL: https://doi.org/10.1007/978-3-319-21070-4_38

Abstract

For many years, formal methods have been used to design and develop critical systems in order to guarantee safety and security and the correctness of desired behaviours, through formal verification and validation techniques and tools. The development of high confidence medical devices such as the cardiac pacemaker, is one of the grand challenges in the area of verified software that need formal reasoning and proof-based development. This paper presents an example of how we used previous experience in developing a cardiac pacemaker using Event-B, to build an incremental proof-based development of a new pacemaker that uses Cardiac Resynchronization Therapy (CRT), also known as biventricular pacing or multisite pacing. In this work, we formalized the required behaviours of CRT including timing constraints and safety properties. We formalized the system using Event-B, and made use of the included Rodin tools to check the internal consistency with respect to safety properties, invariants and events. The system behaviours of the proven model were validated through the use of the ProB model checker.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-02354040
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Other partners > McMaster University (CANADA)
Statistics:download
Deposited By: Neeraj SINGH
Deposited On:07 Nov 2019 14:39

Repository Staff Only: item control page