Quantitative Verification of Implantable Cardiac Pacemakers
Implantable medical devices, such as cardiac pacemakers, must be designed and programmed to the highest levels of safety and reliability. Recently, errors in embedded software have led to a substantial increase in safety alerts, costly device recalls or even patient death. To address such issues, we...
| Huvudupphovsmän: | , , , |
|---|---|
| Materialtyp: | Conference item |
| Publicerad: |
2015
|
| _version_ | 1826283935139627008 |
|---|---|
| author | Chen, T Diciolla, M Kwiatkowska, M Mereacre, A |
| author_facet | Chen, T Diciolla, M Kwiatkowska, M Mereacre, A |
| author_sort | Chen, T |
| collection | OXFORD |
| description | Implantable medical devices, such as cardiac pacemakers, must be designed and programmed to the highest levels of safety and reliability. Recently, errors in embedded software have led to a substantial increase in safety alerts, costly device recalls or even patient death. To address such issues, we propose a model-based framework for quantitative, automated verification of pacemaker software. We adapt the electrocardiogram model of Clifford et al, which generates realistic normal and abnormal heart beat behaviours, with probabilistic transitions between them, to produce a timed sequence of action potential signals that serve as pacemaker input. Working with the timed automata model of the pacemaker by Jiang et al, we develop a methodology for deriving the composition of the heart and the pacemaker, based on discretisation. The main correctness properties we consider include checking that the pacemaker corrects Bradycardia (slow heart beat) and does not induce Tachycardia (fast heart beat), for a range of realistic heart behaviours. We also analyse undersensing, through considering noise on sensor readings, and energy usage. We implement the framework using the probabilistic model checker PRISM and MATLAB and demonstrate encouraging experimental results. Our approach can be adapted to individual patients and is applicable to other pacemaker models. |
| first_indexed | 2024-03-07T01:06:18Z |
| format | Conference item |
| id | oxford-uuid:8b75ffdf-c33e-4469-b197-17f35cd18fe7 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T01:06:18Z |
| publishDate | 2015 |
| record_format | dspace |
| spelling | oxford-uuid:8b75ffdf-c33e-4469-b197-17f35cd18fe72022-03-26T22:38:10ZQuantitative Verification of Implantable Cardiac PacemakersConference itemhttp://purl.org/coar/resource_type/c_5794uuid:8b75ffdf-c33e-4469-b197-17f35cd18fe7Department of Computer Science2015Chen, TDiciolla, MKwiatkowska, MMereacre, AImplantable medical devices, such as cardiac pacemakers, must be designed and programmed to the highest levels of safety and reliability. Recently, errors in embedded software have led to a substantial increase in safety alerts, costly device recalls or even patient death. To address such issues, we propose a model-based framework for quantitative, automated verification of pacemaker software. We adapt the electrocardiogram model of Clifford et al, which generates realistic normal and abnormal heart beat behaviours, with probabilistic transitions between them, to produce a timed sequence of action potential signals that serve as pacemaker input. Working with the timed automata model of the pacemaker by Jiang et al, we develop a methodology for deriving the composition of the heart and the pacemaker, based on discretisation. The main correctness properties we consider include checking that the pacemaker corrects Bradycardia (slow heart beat) and does not induce Tachycardia (fast heart beat), for a range of realistic heart behaviours. We also analyse undersensing, through considering noise on sensor readings, and energy usage. We implement the framework using the probabilistic model checker PRISM and MATLAB and demonstrate encouraging experimental results. Our approach can be adapted to individual patients and is applicable to other pacemaker models. |
| spellingShingle | Chen, T Diciolla, M Kwiatkowska, M Mereacre, A Quantitative Verification of Implantable Cardiac Pacemakers |
| title | Quantitative Verification of Implantable Cardiac Pacemakers |
| title_full | Quantitative Verification of Implantable Cardiac Pacemakers |
| title_fullStr | Quantitative Verification of Implantable Cardiac Pacemakers |
| title_full_unstemmed | Quantitative Verification of Implantable Cardiac Pacemakers |
| title_short | Quantitative Verification of Implantable Cardiac Pacemakers |
| title_sort | quantitative verification of implantable cardiac pacemakers |
| work_keys_str_mv | AT chent quantitativeverificationofimplantablecardiacpacemakers AT diciollam quantitativeverificationofimplantablecardiacpacemakers AT kwiatkowskam quantitativeverificationofimplantablecardiacpacemakers AT mereacrea quantitativeverificationofimplantablecardiacpacemakers |