A Formal Verification Methodology for DDD Mode Pacemaker Control Programs
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 pr...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2015-01-01
|
| Series: | Journal of Electrical and Computer Engineering |
| Online Access: | http://dx.doi.org/10.1155/2015/939028 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850227519262818304 |
|---|---|
| author | Sana Shuja Sudarshan K. Srinivasan Shaista Jabeen Dharmakeerthi Nawarathna |
| author_facet | Sana Shuja Sudarshan K. Srinivasan Shaista Jabeen Dharmakeerthi Nawarathna |
| author_sort | Sana Shuja |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-2bd2be4fe24545199bc5d22ae671b3bc |
| institution | OA Journals |
| issn | 2090-0147 2090-0155 |
| language | English |
| publishDate | 2015-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Electrical and Computer Engineering |
| spelling | doaj-art-2bd2be4fe24545199bc5d22ae671b3bc2025-08-20T02:04:49ZengWileyJournal of Electrical and Computer Engineering2090-01472090-01552015-01-01201510.1155/2015/939028939028A Formal Verification Methodology for DDD Mode Pacemaker Control ProgramsSana Shuja0Sudarshan K. Srinivasan1Shaista Jabeen2Dharmakeerthi Nawarathna3Department of Electrical and Computer Engineering, North Dakota State University, 1411 Centennial Boulevard, Fargo, ND 58102, USADepartment of Electrical and Computer Engineering, North Dakota State University, 1411 Centennial Boulevard, Fargo, ND 58102, USADepartment of Electrical and Computer Engineering, North Dakota State University, 1411 Centennial Boulevard, Fargo, ND 58102, USADepartment of Electrical and Computer Engineering, North Dakota State University, 1411 Centennial Boulevard, Fargo, ND 58102, USAPacemakers 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.http://dx.doi.org/10.1155/2015/939028 |
| spellingShingle | Sana Shuja Sudarshan K. Srinivasan Shaista Jabeen Dharmakeerthi Nawarathna A Formal Verification Methodology for DDD Mode Pacemaker Control Programs Journal of Electrical and Computer Engineering |
| title | A Formal Verification Methodology for DDD Mode Pacemaker Control Programs |
| title_full | A Formal Verification Methodology for DDD Mode Pacemaker Control Programs |
| title_fullStr | A Formal Verification Methodology for DDD Mode Pacemaker Control Programs |
| title_full_unstemmed | A Formal Verification Methodology for DDD Mode Pacemaker Control Programs |
| title_short | A Formal Verification Methodology for DDD Mode Pacemaker Control Programs |
| title_sort | formal verification methodology for ddd mode pacemaker control programs |
| url | http://dx.doi.org/10.1155/2015/939028 |
| work_keys_str_mv | AT sanashuja aformalverificationmethodologyfordddmodepacemakercontrolprograms AT sudarshanksrinivasan aformalverificationmethodologyfordddmodepacemakercontrolprograms AT shaistajabeen aformalverificationmethodologyfordddmodepacemakercontrolprograms AT dharmakeerthinawarathna aformalverificationmethodologyfordddmodepacemakercontrolprograms AT sanashuja formalverificationmethodologyfordddmodepacemakercontrolprograms AT sudarshanksrinivasan formalverificationmethodologyfordddmodepacemakercontrolprograms AT shaistajabeen formalverificationmethodologyfordddmodepacemakercontrolprograms AT dharmakeerthinawarathna formalverificationmethodologyfordddmodepacemakercontrolprograms |