More Web Proxy on the site http://driver.im/

short-paper

Public Access

Towards Model Checking of Implantable Cardioverter Defibrillators

Authors:

Rahul MangharamAuthors Info & Claims

HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

Pages 87 - 92

https://doi.org/10.1145/2883817.2883841

Published: 11 April 2016 Publication History

Abstract

Ventricular Fibrillation is a disorganized electrical excitation of the heart that results in inadequate blood flow to the body. It usually ends in death within a minute. A common way to treat the symptoms of fibrillation is to implant a medical device, known as an Implantable Cardioverter Defibrillator (ICD), in the patient's body. Model-based verification can supply rigorous proofs of safety and efficacy. In this paper, we build a hybrid system model of the human heart+ICD closed loop, and show it to be a STORMED system, a class of o-minimal hybrid systems that admit finite bisimulations. In general, it may not be possible to compute the bisimulation. We show that approximate reachability can yield a finite simulation for STORMED systems, and that certain compositions respect the STORMED property. The results of this paper are theoretical and motivate the creation of concrete model checking procedures for STORMED systems.

References

[1]

H. Abbas, K. J. Jang, Z. Jiang, and R. Mangharam. Model checking implantable cardioverter defibrillators. 2016. Arxiv 1512.08083.

Digital Library

[2]

E. Bartocci, F. Corradini, M. D. Berardini, E. Entcheva, S. Smolka, and R. Grosu. Modeling and simulation of cardiac tissue using hybrid I/O automata. Th. Com. Sci., 410(33), 2009.

Digital Library

[3]

Boston Scientific Corporation. The Compass - Technical Guide to Boston Scientific Cardiac Rhythm Management Products. Device Documentation, 2007.

[4]

T. Chen, M. Diciolla, M. Kwiatkowska, and A. Mereacre. Quantitative verification of implantable cardiac pacemakers over hybrid heart models. Information and Computation, 236:87 -- 101, 2014.

Digital Library

[5]

D. D. Correa de Sa, N. Thompson, J. Stinnett-Donnelly, P. Znojkiewicz, N. Habel, J. G. Muller, J. H. Bates, J. S. Buzas, and P. S. Spector. Electrogram fractionation. Circ Arrhythm Electrophysiol, 55:909 -- 916, Dec 2011.

[6]

R. Hood. The EP Lab. Accessed 10/20/2015.

[7]

Z. Huang, C. Fan, A. Mereacre, S. Mitra, and M. Kwiatkowska. Invariant verification of nonlinear hybrid automata networks of cardiac cells. In A. Biere and R. Bloem, editors, CAV. 2014.

Digital Library

[8]

M. A. Islam, R. DeFrancisco, C. Fan, R. Grosu, S. Mitra, and S. Smolka. Model checking tap withdrawal in c. elegans. In HSB. 2015.

[9]

M. A. Islam, A. Murthy, A. Girard, S. A. Smolka, and R. Grosu. Compositionality results for cardiac cell dynamics. HSCC, 2014.

Digital Library

[10]

R. Klabunde. Cardiovascular electrophysiology concepts. Lippincott-Williams, 2 edition, 2011.

[11]

G. Lafferriere, G. J. Pappas, and S. Sastry. O-minimal hybrid systems. Mathematics of Control, Signals and Systems, 13(1):1--21, 2000.

[12]

M. Pajic, Z. Jiang, I. Lee, O. Sokolsky, and R. Mangharam. Safety-critical medical device development using the upp2sf model translation tool. ACM Trans. Embed. Comput. Syst., 13(4), 2014.

Digital Library

[13]

P. S. Spector. Visible EP. Accessed 10/20/2015.

[14]

P. S. Spector, N. Habel, B. E. Sobel, and J. H. Bates. Emergence of complex behavior: An interactive model of cardiac excitation provides a powerful tool for understanding electric propagation. Circulation: Arrhythmia and Electrophysiology, 4(4):586--591, 2011.

[15]

V. Vladimerou, P. Prabhakar, M. Viswanathan, and G. Dullerud. Stormed hybrid systems. In Automata, Languages and Programming. 2008.

Digital Library

Cited By

S NK VNL P(2023)A COMPARATIVE STUDY OF MEDICAL DEVICES AND THEIR REGULATIONS IN US, EU, INDIA, AND CHINAAsian Journal of Pharmaceutical and Clinical Research10.22159/ajpcr.2023.v16i3.46624(6-14)Online publication date: 7-Mar-2023
https://doi.org/10.22159/ajpcr.2023.v16i3.46624
Ai WPatel NRoop PMalik ATrew M(2020)Cardiac Electrical Modeling for Closed-Loop Validation of Implantable DevicesIEEE Transactions on Biomedical Engineering10.1109/TBME.2019.291721267:2(536-544)Online publication date: Feb-2020
https://doi.org/10.1109/TBME.2019.2917212
Abbas HMangharam R(2018)Generalized Robust MTL Semantics for Problems in Cardiac Electrophysiology2018 Annual American Control Conference (ACC)10.23919/ACC.2018.8431460(1592-1597)Online publication date: Jun-2018
https://doi.org/10.23919/ACC.2018.8431460
Show More Cited By

Index Terms

Towards Model Checking of Implantable Cardioverter Defibrillators
1. Applied computing
  1. Life and medical sciences
2. Computing methodologies
  1. Modeling and simulation
    1. Model development and analysis

Recommendations

Fuzzy logic-based diagnostic algorithm for implantable cardioverter defibrillators

Objective: The paper presents a diagnostic algorithm for classifying cardiac tachyarrhythmias for implantable cardioverter defibrillators (ICDs). The main aim was to develop an algorithm that could reduce the rate of occurrence of inappropriate ...
Cost-Effectiveness of Implantable Cardioverter-Defibrillators in Brugada Syndrome Treatment

Brugada syndrome is characterized by an ST-segment elevation in the right precordial ECG leads and a high incidence of sudden death in patients with structurally normal hearts. Some trials have demonstrated that the cost-effectiveness of ICD ...
Real-Time Heart Model for Implantable Cardiac Device Validation and Verification
ECRTS '10: Proceedings of the 2010 22nd Euromicro Conference on Real-Time Systems

Designing bug-free medical device software is challenging, especially in complex implantable devices that may be used in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems between ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

April 2016

324 pages

ISBN:9781450339551

DOI:10.1145/2883817

Program Chairs:
Alessandro Abate
University of Oxford, UK
,
Georgios Fainekos
Arizona State University, USA

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper

Funding Sources

Conference

HSCC'16

Sponsor:

SIGBED

HSCC'16: 19th International Conference on Hybrid Systems: Computation and Control

April 12 - 14, 2016

Vienna, Austria

Acceptance Rates

HSCC '16 Paper Acceptance Rate 28 of 65 submissions, 43%;

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
338
Total Downloads

Downloads (Last 12 months)87
Downloads (Last 6 weeks)6

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

S NK VNL P(2023)A COMPARATIVE STUDY OF MEDICAL DEVICES AND THEIR REGULATIONS IN US, EU, INDIA, AND CHINAAsian Journal of Pharmaceutical and Clinical Research10.22159/ajpcr.2023.v16i3.46624(6-14)Online publication date: 7-Mar-2023
https://doi.org/10.22159/ajpcr.2023.v16i3.46624
Ai WPatel NRoop PMalik ATrew M(2020)Cardiac Electrical Modeling for Closed-Loop Validation of Implantable DevicesIEEE Transactions on Biomedical Engineering10.1109/TBME.2019.291721267:2(536-544)Online publication date: Feb-2020
https://doi.org/10.1109/TBME.2019.2917212
Abbas HMangharam R(2018)Generalized Robust MTL Semantics for Problems in Cardiac Electrophysiology2018 Annual American Control Conference (ACC)10.23919/ACC.2018.8431460(1592-1597)Online publication date: Jun-2018
https://doi.org/10.23919/ACC.2018.8431460
Andalam SAllen NMalik ARoop PTrew M(2017)A Novel Emulation Model of the Cardiac Conduction SystemACM Transactions on Embedded Computing Systems10.1145/312654216:5s(1-20)Online publication date: 27-Sep-2017
https://dl.acm.org/doi/10.1145/3126542

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents