A Formal Verification Methodology for DDD Mode Pacemaker Control Programs
Joint Authors
Shuja, Sana
Jabeen, Shaista
Nawarathna, Dharmakeerthi
Srinivasan, Sudarshan K.
Source
Journal of Electrical and Computer Engineering
Issue
Vol. 2015, Issue 2015 (31 Dec. 2015), pp.1-10, 10 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2015-09-01
Country of Publication
Egypt
No. of Pages
10
Main Subjects
Information Technology and Computer Science
Abstract EN
Pacemakers are safety-critical devices whose faulty behaviors can cause harm or even death.
Often these faulty behaviors are caused due to bugs in programs used for digital control of pacemakers.
We present a formal verification methodology that can be used to check the correctness of object code programs that implement the safety-critical control functions of DDD mode pacemakers.
Our methodology is based on the theory of Well-Founded Equivalence Bisimulation (WEB) refinement, where both formal specifications and implementation are treated as transition systems.
We develop a simple and general formal specification for DDD mode pacemakers.
We also develop correctness proof obligations that can be applied to validate object code programs used for pacemaker control.
Using our methodology, we were able to verify a control program with millions of transitions against the simple specification with only 10 transitions.
Our method also found several bugs during the verification process.
American Psychological Association (APA)
Shuja, Sana& Srinivasan, Sudarshan K.& Jabeen, Shaista& Nawarathna, Dharmakeerthi. 2015. A Formal Verification Methodology for DDD Mode Pacemaker Control Programs. Journal of Electrical and Computer Engineering،Vol. 2015, no. 2015, pp.1-10.
https://search.emarefa.net/detail/BIM-1068163
Modern Language Association (MLA)
Shuja, Sana…[et al.]. A Formal Verification Methodology for DDD Mode Pacemaker Control Programs. Journal of Electrical and Computer Engineering No. 2015 (2015), pp.1-10.
https://search.emarefa.net/detail/BIM-1068163
American Medical Association (AMA)
Shuja, Sana& Srinivasan, Sudarshan K.& Jabeen, Shaista& Nawarathna, Dharmakeerthi. A Formal Verification Methodology for DDD Mode Pacemaker Control Programs. Journal of Electrical and Computer Engineering. 2015. Vol. 2015, no. 2015, pp.1-10.
https://search.emarefa.net/detail/BIM-1068163
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-1068163