Abstract
Rate-adaptive pacemakers are cardiac devices able to automatically adjust the pacing rate in patients with chronotropic incompetence, i.e., whose heart is unable to provide an adequate rate at increasing levels of physical, mental, or emotional activity. These devices work by processing data from physiological sensors in order to detect the patient’s activity and update the pacing rate accordingly. Rate adaptation parameters depend on many patient-specific factors, and effective personalization of such treatments can only be achieved through extensive exercise testing, which is normally intolerable for a cardiac patient. In this work, we introduce a data-driven and model-based approach for the automated verification of rate-adaptive pacemakers and formal analysis of personalized treatments. To this purpose, we develop a novel dual-sensor pacemaker model where the adaptive rate is computed by blending information from an accelerometer, and a metabolic sensor based on the QT interval. Our approach enables personalization through the estimation of heart model parameters from patient data (electrocardiogram), and closed-loop analysis through the online generation of synthetic, model-based QT intervals and acceleration signals. In addition to personalization, we also support the derivation of models able to account for the varied characteristics of a virtual patient population, thus enabling safety verification of the device. To capture the probabilistic and nonlinear dynamics of the heart, we define a probabilistic extension of timed I/O automata with data and employ statistical model checking for quantitative verification of rate modulation. We evaluate our rate-adaptive pacemaker design on three subjects and a pool of virtual patients, demonstrating the potential of our approach to provide rigorous, quantitative insights into the closed-loop behavior of the device under different exercise levels and heart conditions.
Supplemental Material
Available for Download
Supplemental movie, appendix, image and software files for, Closed-Loop Quantitative Verification of Rate-Adaptive Pacemakers
- Freddy M. Abi-Samra, Narendra Singh, Benjamin L. Rosin, Jerome V. Dwyer, Crystal D. Miller, and CLEAR Study Investigators. 2013. Effect of rate-adaptive pacing on performance and physiological parameters during activities of daily living in the elderly: Results from the CLEAR (cylos responds with physiologic rate changes during daily activities) study. Europace 15, 6 (2013), 849--856.Google ScholarCross Ref
- Staffan Ahnve and Hans Vallin. 1982. Influence of heart rate and inhibition of autonomic tone on the QT interval. Circulation 65, 3 (1982), 435--439.Google ScholarCross Ref
- Weiwei Ai, Nitish Patel, and Partha Roop. 2016. Requirements-centric closed-loop validation of implantable cardiac devices. In Design, Automation 8 Test in Europe Conference 8 Exhibition (DATE’16). IEEE, 846--849. Google ScholarDigital Library
- Weiwei Ai, Nitish D. Patel, Partha S. Roop, Avinash Malik, Sidharta Andalam, Eugene Yip, Nathan Allen, and Mark L. Trew. 2018. A parametric computational model of the action potential of pacemaker cells. IEEE Transactions on Biomedical Engineering 65, 1 (2018), 123--130.Google ScholarCross Ref
- Paul Albrecht. 1983. ST Segment Characterization for Long Term Automated ECG Analysis. PhD Thesis. Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science.Google Scholar
- Rajeev Alur. 1999. Timed automata. In International Conference on Computer Aided Verification. Springer, 8--22. Google ScholarDigital Library
- Francesco Amigoni, Alessandro Beda, and Nicola Gatti. 2006. Combining rate-adaptive cardiac pacing algorithms via multiagent negotiation. IEEE Transactions on Information Technology in Biomedicine 10, 1 (2006), 11--18. Google ScholarDigital Library
- Davide Anguita, Alessandro Ghio, Luca Oneto, Xavier Parra, and Jorge L. Reyes-Ortiz. 2013. A public domain dataset for human activity recognition using smartphones. In European Symposium on Artificial Neural Networks, Computational Intelligence and Machine Learning (ESANN’13).Google Scholar
- Paolo Ballarini, Benoît Barbot, Marie Duflot, Serge Haddad, and Nihal Pekergin. 2015. HASL: A new approach for performance evaluation and model checking from concepts to experimentation. Performance Evaluation 90 (2015), 53--77. Google ScholarDigital Library
- Benoît Barbot, Marta Kwiatkowska, Alexandru Mereacre, and Nicola Paoletti. 2015a. Estimation and verification of hybrid heart models for personalised medical and wearable devices. In Computational Methods in Systems Biology (LNCS), Vol. 9308. Springer, 3--7.Google Scholar
- Benoît Barbot, Marta Kwiatkowska, Alexandru Mereacre, and Nicola Paoletti. 2015b. Estimation and Verification of Hybrid Heart Models for Personalised Medical and Wearable Devices. Technical Report CS-RR-15-05. Department of Computer Science, University of Oxford.Google Scholar
- Benoît Barbot, Marta Kwiatkowska, Alexandru Mereacre, and Nicola Paoletti. 2016. Building power consumption models from executable timed I/O automata specifications. In Hybrid Systems: Computation and Control (HSCC’16). ACM, 195--204. Google ScholarDigital Library
- Chris Barker, Marta Kwiatkowska, Alexandru Mereacre, Nicola Paoletti, and Andrea Patanè. 2015. Hardware-in-the-loop simulation and energy optimization of cardiac pacemakers. In IEEE Engineering in Medicine and Biology Society (EMBC’15). IEEE, 7188--7191.Google Scholar
- Ezio Bartocci, Flavio Corradini, Maria Rita Di Berardini, Emilia Entcheva, Scott A. Smolka, and Radu Grosu. 2009. Modeling and simulation of cardiac tissue using hybrid i/o automata. Theoretical Computer Science 410, 33 (2009), 3149--3165. Google ScholarDigital Library
- Alan D. Bernstein, Jean-Claude Daubert, Ross D. Fletcher, David L. Hayes, Berndt Lüderitz, Dwight W. Reynolds, Mark H. Schoenfeld, and Richard Sutton. 2002. The revised NASPE/BPEG generic code for antibradycardia, adaptive-rate, and multisite pacing. Pacing and Clinical Electrophysiology 25, 2 (2002), 260--264.Google ScholarCross Ref
- Adam Bohm, Robert Kiss, Paul Dorian, and Arnold Pinter. 2010. Single-chamber, rate-responsive pacemaker-mediated tachycardia. Canadian Journal of Cardiology 26, 9 (2010), e340.Google ScholarCross Ref
- Reto Candinas, Markus Jakob, Thomas A. Buckingham, Heidy Mattmann, and F. Wolfgang Amann. 1997. Vibration, acceleration, gravitation, and movement: Activity controlled rate adaptive pacing during treadmill exercise testing and daily life activities. Pacing and Clinical Electrophysiology 20, 7 (1997), 1777--1786.Google ScholarCross Ref
- Taolue Chen, Marco Diciolla, Marta Kwiatkowska, and Alexandru Mereacre. 2014. Quantitative verification of implantable cardiac pacemakers over hybrid heart models. Information and Computation 236 (2014), 87--101. Google ScholarDigital Library
- Saisakul Chernbumroong, Anthony S. Atkins, and Hongnian Yu. 2011. Activity classification using a single wrist-worn accelerometer. In 2011 5th International Conference on Software, Knowledge Information, Industrial Management and Applications (SKIMA’11). IEEE, 1--6.Google ScholarCross Ref
- Patrick Davey and Jeffrey Bateman. 1999. Heart rate and catecholamine contribution to QT interval shortening on exercise. Clinical Cardiology 22, 8 (1999), 513--518.Google ScholarCross Ref
- Simonetta Dell’Orto, Paolo Valli, and Enrico Maria Greco. 2004. Sensors for rate responsive pacing. Indian Pacing and Electrophysiology Journal 4, 3 (2004), 137.Google Scholar
- Simon Eberz, Nicola Paoletti, Marc Roeschlin, Andrea Patanè, Marta Kwiatkowska, and Ivan Martinovic. 2017. Broken hearted: How to attack ECG biometrics. In Network and Distributed System Security Symposium.Google ScholarCross Ref
- Kenneth A. Ellenbogen, Bruce L. Wilkoff, G. Neal Kay, Chu Pak Lau, and Angelo Auricchio. 2016. Clinical Cardiac Pacing, Defibrillation and Resynchronization Therapy. Elsevier Health Sciences.Google Scholar
- Ary L. Goldberger, Luis A. N. Amaral, Leon Glass, Jeffrey M. Hausdorff, Plamen Ch. Ivanov, Roger G. Mark, Joseph E. Mietus, George B. Moody, Chung-Kang Peng, and H. Eugene Stanley. 2000. Physiobank, physiotoolkit, and physionet components of a new research resource for complex physiologic signals. Circulation 101, 23 (2000), e215--e220.Google ScholarCross Ref
- Artur Oliveira Gomes and Marcel Vinicius Medeiros Oliveira. 2009. Formal specification of a cardiac pacing system. In Formal Methods (FM’09). Springer, 692--707. Google ScholarDigital Library
- Radu Grosu, Gregory Batt, Flavio H. Fenton, James Glimm, Colas Le Guernic, Scott A. Smolka, and Ezio Bartocci. 2011. From cardiac cells to genetic regulatory networks. In Computer Aided Verification. Springer, 396--411. Google ScholarDigital Library
- John R. Hampton and David Adlam. 2013. The ECG in Practice. Elsevier Health Sciences.Google Scholar
- Paul A. Iaizzo. 2009. Handbook of Cardiac Anatomy, Physiology, and Devices. Springer Science 8 Business Media.Google Scholar
- Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, and Rahul Mangharam. 2012. Modeling and verification of a dual chamber implantable pacemaker. In Tools and Algorithms for the Construction and Analysis of Systems. Springer, 188--203. Google ScholarDigital Library
- Tamara G. Kolda, Robert Michael Lewis, and Virginia Torczon. 2003. Optimization by direct search: New perspectives on some classical and modern methods. SIAM Review 45, 3 (2003), 385--482.Google ScholarCross Ref
- Marta Kwiatkowska, Harriet Lea-Banks, Alexandru Mereacre, and Nicola Paoletti. 2014. Formal modelling and validation of rate-adaptive pacemakers. In 2014 IEEE International Conference on Healthcare Informatics (ICHI’14). IEEE, 23--32. Google ScholarDigital Library
- Marta Kwiatkowska, Alexandru Mereacre, Nicola Paoletti, and Andrea Patanè. 2015. Synthesising robust and optimal parameters for cardiac pacemakers using symbolic and evolutionary computation techniques. In Hybrid Systems and Biology (HSB’15) (LNCS/LNBI), Vol. 9271. Springer, 119--140.Google Scholar
- Gervasio A. Lamas, J. David Knight, Michael O. Sweeney, Marcus Mianulli, Vinod Jorapur, Koroush Khalighi, James R. Cook, Russell Silverman, Lawrence Rosenthal, Nancy Clapp-Channing, Kerry L. Lee, and Daniel B. Mark. 2007. Impact of rate-modulated pacing on quality of life and exercise capacity evidence from the advanced elements of pacing randomized controlled trial (ADEPT). Heart Rhythm 4, 9 (2007), 1125--1132.Google ScholarCross Ref
- Chu-Pak Lau, Hung-Fat Tse, A. John Camm, and Serge S. Barold. 2007. Evolution of pacing for bradycardias: Sensors. European Heart Journal Supplements 9, suppl I (2007), I11--I22.Google ScholarCross Ref
- Jie Lian, Hannes Krätschmer, Dirk Müssig, and L. Stotts. 2010. Open source modeling of heart rhythm and cardiac pacing. Open Pacing Electrophysiology Therapy Journal 3 (2010), 4.Google Scholar
- Jie Lian, D. Mussig, and Volker Lang. 2006. Computer modeling of ventricular rhythm during atrial fibrillation and ventricular pacing. IEEE Transactions on Biomedical Engineering 53, 8 (2006), 1512--1520.Google ScholarCross Ref
- Hugo Daniel Macedo, Peter Gorm Larsen, and John Fitzgerald. 2008. Incremental development of a distributed real-time model of a cardiac pacing system using VDM. In Formal Methods. 181. Google ScholarDigital Library
- Anthony R. Magnano, Steve Holleran, Rajasekhar Ramakrishnan, James A. Reiffel, and Daniel M. Bloomfield. 2002. Autonomic nervous system influences on QT interval in normal subjects. Journal of the American College of Cardiology 39, 11 (2002), 1820--1826.Google ScholarCross Ref
- Merak Malik, P. Färbom, V. Batchvarov, K. Hnatkova, and A. J. Camm. 2002. Relation between QT and RR intervals is highly individual among healthy subjects: Implications for heart rate correction of the QT interval. Heart 87, 3 (2002), 220--228.Google ScholarCross Ref
- Jaakko Malmivuo and Robert Plonsey. 1995. Bioelectromagnetism: Principles and Applications of Bioelectric and Biomagnetic Fields. Oxford University Press.Google ScholarCross Ref
- Vias Markides and Richard J. Schilling. 2003. Atrial fibrillation: Classification, pathophysiology, mechanisms and drug treatment. Heart 89, 8 (2003), 939--943.Google ScholarCross Ref
- Patrick E. McSharry, Gari D. Clifford, Lionel Tarassenko, and Leonard A. Smith. 2003. A dynamical model for generating synthetic electrocardiogram signals. IEEE Transactions on Biomedical Engineering 50, 3 (2003), 289--294.Google ScholarCross Ref
- Dominique Méry, Bernhard Schätz, and Alan Wassyng. 2014. The pacemaker challenge: Developing certifiable medical devices (Dagstuhl seminar 14062). Dagstuhl Reports 4, 2 (2014), 17--37.Google Scholar
- Dominique Méry and Neeraj Kumar Singh. 2009. Pacemaker’s Functional Behaviors in Event-B. Rapport de recherche. Retrieved from http://hal.inria.fr/inria-00419973.Google Scholar
- Benjamin Monteil, Sylvain Ploux, Romain Eschalier, Philippe Ritter, Michel Haissaguerre, Jayanthi N. Koneru, Kenneth A. Ellenbogen, and Pierre Bordachar. 2015. Pacemaker-mediated tachycardia: Manufacturer specifics and spectrum of cases. Pacing and Clinical Electrophysiology 38, 12 (2015), 1489--1498.Google ScholarCross Ref
- Kazunori Ohkawara, Yoshitake Oshima, Yuki Hikihara, Kazuko Ishikawa-Takata, Izumi Tabata, and Shigeho Tanaka. 2011. Real-time estimation of daily physical activity intensity by a triaxial accelerometer and a gravity-removal classification algorithm. British Journal of Nutrition 105 (6 2011), 1681--1691.Google Scholar
- Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, and Rahul Mangharam. 2012. From verification to implementation: A model translation tool and a pacemaker case study. In 2012 IEEE 18th Real-Time and Embedded Technology and Applications Symposium (RTAS’12). IEEE, 173--184. Google ScholarDigital Library
- Jiapu Pan and Willis J. Tompkins. 1985. A real-time QRS detection algorithm. IEEE Transactions on Biomedical Engineering 3 (1985), 230--236.Google ScholarCross Ref
- John W. Poore and Brian M. Mann. 1991. Self-adjusting rate-responsive pacemaker and method thereof. Retrieved from https://www.google.co.uk/patents/US5074302. US Patent 5,074,302.Google Scholar
- Reza Sameni, Mohammad B. Shamsollahi, Christian Jutten, and Gari D. Clifford. 2007. A nonlinear bayesian filtering framework for ECG denoising. IEEE Transactions on Biomedical Engineering 54, 12 (2007), 2172--2185.Google ScholarCross Ref
- Dominic P. Searson. 2015. GPTIPS 2: An open-source software platform for symbolic data mining. In Handbook of Genetic Programming Applications. Springer.Google Scholar
- Jae-Woo Shin, Jung-Han Yoon, and Y. R. Yoon. 2001. Rate-adaptive pacemaker controlled by motion and respiratory rate using neuro-fuzzy algorithm. Medical and Biological Engineering and Computing 39, 6 (2001), 694--699.Google ScholarCross Ref
- Hirofumi Tanaka, Kevin D. Monahan, and Douglas R. Seals. 2001. Age-predicted maximal heart rate revisited. Journal of the American College of Cardiology 37, 1 (2001), 153--156.Google ScholarCross Ref
- Luu Anh Tuan, Man Chun Zheng, and Quan Thanh Tho. 2010. Modeling and verification of safety critical systems: A case study on pacemaker. In 2010 4th International Conference on Secure Software Integration and Reliability Improvement (SSIRI’10). IEEE, 23--32. Google ScholarDigital Library
- Jin Wang, Ronghua Chen, Xiangping Sun, Mary F. H. She, and Yuchuan Wu. 2011. Recognizing human daily activities from accelerometer signal. Procedia Engineering 15 (2011), 1780--1786.Google ScholarCross Ref
- Bruce L. Wilkoff, Joseph Corey, and Gordon Blackburn. 1989. A mathematical model of the cardiac chronotropic response to exercise. Journal of Electrophysiology 3, 3 (1989), 176--180.Google ScholarCross Ref
- Pei Ye, Emilia Entcheva, Radu Grosu, and Scott A. Smolka. 2005. Efficient modeling of excitable cells using hybrid automata. In Proceedings of the 3rd International Conference on Computational Methods in Systems Biology, Vol. 5. 216--227.Google Scholar
- Håkan L. S. Younes, Marta Kwiatkowska, Gethin Norman, and David Parker. 2006. Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer 8, 3 (2006), 216--228.Google ScholarDigital Library
Index Terms
- Closed-Loop Quantitative Verification of Rate-Adaptive Pacemakers
Recommendations
A simulink hybrid heart model for quantitative verification of cardiac pacemakers
HSCC '13: Proceedings of the 16th international conference on Hybrid systems: computation and controlWe develop a novel hybrid heart model in Simulink that is suitable for quantitative verification of implantable cardiac pacemakers. The heart model is formulated at the level of cardiac cells, can be adapted to patient data, and incorporates ...
Development of closed-loop modelling framework for adaptive respiratory pacemakers
Abstract ObjectiveVentilatory pacing by electrical stimulation of the phrenic nerve has many advantages compared to mechanical ventilation. However, commercially available respiratory pacing devices operate in an open-loop fashion, ...
Highlights- Systematic closed-loop modelling framework for adaptive respiratory pacemakers.
Quantitative verification of implantable cardiac pacemakers over hybrid heart models
We develop a model-based framework which supports approximate quantitative verification of implantable cardiac pacemaker models over hybrid heart models. The framework is based on hybrid input-output automata and can be instantiated with user-specified ...
Comments