skip to main content
research-article

Automated closed-loop model checking of implantable pacemakers using abstraction trees

Published: 31 March 2017 Publication History

Abstract

Autonomous medical devices such as implantable cardiac pacemakers are capable of diagnosing the patient condition and delivering therapy without human intervention. Their ability to autonomously affect the physiological state of the patient makes them safety-critical. Sufficient evidence for the safety and efficacy of the device software, which makes these autonomous decisions, should be provided before these devices can be released on the market. Formal methods like model checking can provide safety evidence that the devices can safely operate under a large variety of physiological conditions. The challenge is to develop physiological models that are general enough to cover the large variability of human physiology, and also expressive enough to provide physiological contexts to counter-examples returned by the model checker. In this paper, the authors develop a set of physiological abstraction rules that introduce physiological constraints to heart models. By applying these abstraction rules to a initial set of heart models, an abstraction tree is created. The root model covers all possible inputs to a pacemaker and derived models cover inputs from different heart conditions. If a counter-example is returned by the model checker, the abstraction tree is traversed so that the most concrete counter-example(s) with physiological contexts can be returned to the domain experts for validity check. The abstraction tree framework replaces the manual abstraction and refinement framework, which reduced the amount of domain knowledge required to perform closed-loop model checking. It encourages the use of model checking during the development of autonomous medical devices, and identifies safety risks earlier in the design process. 1

References

[1]
R. Alur and D. L. Dill. A Theory of Timed Automata. Theoretical Computer Science, 126:183--235, 1994.
[2]
P. Bogdan, S. Jain, and R. Marculescu. Pacemaker control of heart rate variability: A cyber physical system perspective. ACM Transactions on Embedded Computing Systems, 12(1s):50:1--50:22, 2013.
[3]
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counter Example-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM, 50(5):752--794, 2003.
[4]
R. Grosu, G. Batt, F. H. Fenton, J. Glimm, C. Le Guernic, S. Smolka, and E. Bartocci. From cardiac cells to genetic regulatory networks. In Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pages 396--411. Springer Berlin Heidelberg, 2011.
[5]
R. G. Hauser and B. J. Maron. "lessons from the failure and recall of an implantable cardioverter-defibrillator". "American Heart Association, Circulation", pages 2040--2042, 2005.
[6]
Ihor Gussak and Charles Antzelevitch and Arthur A.M. Wilde and Brian D. Powell and Michael J. Ackerman and Win-Kuang Shen. Electrical Diseases of the Heart: Volume 1: Basic Foundations and Primary Electrical Diseases. Springer, 2013.
[7]
M. A. Islam, A. Murthy, A. Girard, S. A. Smolka, and R. Grosu. Compositionality results for cardiac cell dynamics. In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, (HSCC '14), pages 243--252, 2014.
[8]
Z. Jiang, H. Abbas, P. Mosterman, and R. Mangharam. Abstraction-Tree For Closed-loop Model Checking of Medical Devices. Tech Report: http://repository.upenn.edu/mlab_papers/73, 2015.
[9]
Z. Jiang, A. Connolly, and R. Mangharam. Using the Virtual Heart Model to Validate the Mode-Switch Pacemaker Operation. IEEE Engineering in Medicine and Biology Society, pages 6690 --6693, 2010.
[10]
Z. Jiang, M. Pajic, R. Alur, and R. Mangharam. Closed-loop verification of medical devices with model abstraction and refinement. International Journal on Software Tools for Technology Transfer, pages 1--23, 2013.
[11]
M. Josephson. Clinical Cardiac Electrophysiology. Lippincot Williams and Wilkins, 2008.
[12]
K. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer (STTT), 1997.
[13]
A. Murthy, E. Bartocci, F. H. Fenton, J. Glimm, R. A. Gray, E. M. Cherry, S. A. Smolka, and R. Grosu. Curvature analysis of cardiac excitation wavefronts. IEEE/ACM Transactions on Computational Biology and Bioinformatics, 10(2):323--336, 2013.
[14]
S. Rossi, R. Ruiz-Baier, L. F. Pavarino, and A. Quarteroni. Active strain and activation models in cardiac electromechanics. Proceedings in Applied Mathematics and Mechanics (PAMM), 11(1):119--120, 2011.
[15]
F. B. Sachse, A. P. Moreno, and J. A. Abildskov. Electrophysiological modeling of fibroblasts and their interaction with myocytes. Annals of Biomedical Engineering, 36(1):41--56, 2008.
[16]
K. Sandler, L. Ohrstrom, and R. McVay. Killed by Code: Software Transparency in Implantable Medical Devices. Software Freedom Law Center, 2010.
[17]
N. A. Trayanova and P. M. Boyle. Advances in modeling ventricular arrhythmias: from mechanisms to the clinic. Wiley Interdisciplinary Reviews: Systems Biology and Medicine, 6(2):209--224, 2014.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGBED Review
ACM SIGBED Review  Volume 14, Issue 2
Special Issue on Medical Cyber Physical Systems workshop (MedicalCPS'16)
March 2017
53 pages
EISSN:1551-3688
DOI:10.1145/3076125
Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 March 2017
Published in SIGBED Volume 14, Issue 2

Check for updates

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)17
  • Downloads (Last 6 weeks)1
Reflects downloads up to 07 Jan 2025

Other Metrics

Citations

Cited By

View all

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media