{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T10:31:41Z","timestamp":1777458701929,"version":"3.51.4"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,8,9]],"date-time":"2018-08-09T00:00:00Z","timestamp":1533772800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1446832"],"award-info":[{"award-number":["CNS-1446832"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["PoC-620196, AdG-246967"],"award-info":[{"award-number":["PoC-620196, AdG-246967"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2018,10,31]]},"abstract":"<jats:p>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\u2019s 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.<\/jats:p>","DOI":"10.1145\/3152767","type":"journal-article","created":{"date-parts":[[2018,8,9]],"date-time":"2018-08-09T15:25:51Z","timestamp":1533828351000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Closed-Loop Quantitative Verification of Rate-Adaptive Pacemakers"],"prefix":"10.1145","volume":"2","author":[{"given":"Nicola","family":"Paoletti","sequence":"first","affiliation":[{"name":"University of Oxford, Department of Computer Science, Egham Hill, Egham, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Patan\u00e8","sequence":"additional","affiliation":[{"name":"University of Catania, Department of Mathematics and Computer Science"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[{"name":"University of Oxford, Department of Computer Science, Egham Hill, Egham, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,8,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/europace\/eus425"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1161\/01.CIR.65.3.435"},{"key":"e_1_2_2_3_1","volume-title":"Design, Automation 8 Test in Europe Conference 8 Exhibition (DATE\u201916)","author":"Ai Weiwei"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TBME.2017.2695537"},{"key":"e_1_2_2_5_1","unstructured":"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.  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."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733787"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TITB.2005.855564"},{"key":"e_1_2_2_8_1","volume-title":"European Symposium on Artificial Neural Networks, Computational Intelligence and Machine Learning (ESANN\u201913)","author":"Anguita Davide"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2015.04.003"},{"key":"e_1_2_2_10_1","volume-title":"Computational Methods in Systems Biology (LNCS)","author":"Barbot Beno\u00eet"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883844"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Chris Barker Marta Kwiatkowska Alexandru Mereacre Nicola Paoletti and Andrea Patan\u00e8. 2015. Hardware-in-the-loop simulation and energy optimization of cardiac pacemakers. In IEEE Engineering in Medicine and Biology Society (EMBC\u201915). IEEE 7188--7191.  Chris Barker Marta Kwiatkowska Alexandru Mereacre Nicola Paoletti and Andrea Patan\u00e8. 2015. Hardware-in-the-loop simulation and energy optimization of cardiac pacemakers. In IEEE Engineering in Medicine and Biology Society (EMBC\u201915). IEEE 7188--7191.","DOI":"10.1109\/EMBC.2015.7320050"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.02.042"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1046\/j.1460-9592.2002.00260.x"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0828-282X(10)70457-8"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1540-8159.1997.tb03566.x"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.01.014"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SKIMA.2011.6089975"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1002\/clc.4960220805"},{"key":"e_1_2_2_21_1","first-page":"137","article-title":"Sensors for rate responsive pacing","volume":"4","author":"Dell\u2019Orto Simonetta","year":"2004","journal-title":"Indian Pacing and Electrophysiology Journal"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23408"},{"key":"e_1_2_2_23_1","unstructured":"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.  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."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1161\/01.CIR.101.23.e215"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_44"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"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.   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.","DOI":"10.1007\/978-3-642-22110-1_31"},{"key":"e_1_2_2_27_1","unstructured":"John R. Hampton and David Adlam. 2013. The ECG in Practice. Elsevier Health Sciences.  John R. Hampton and David Adlam. 2013. The ECG in Practice. Elsevier Health Sciences."},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Paul A. Iaizzo. 2009. Handbook of Cardiac Anatomy Physiology and Devices. Springer Science 8 Business Media.  Paul A. Iaizzo. 2009. Handbook of Cardiac Anatomy Physiology and Devices. Springer Science 8 Business Media.","DOI":"10.1007\/978-1-60327-372-5"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_14"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1137\/S003614450242889"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICHI.2014.11"},{"key":"e_1_2_2_32_1","volume-title":"Hybrid Systems and Biology (HSB\u201915) (LNCS\/LNBI)","author":"Kwiatkowska Marta"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.hrthm.2007.05.021"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1093\/eurheartj\/sum057"},{"key":"e_1_2_2_35_1","first-page":"4","article-title":"Open source modeling of heart rhythm and cardiac pacing","volume":"3","author":"Lian Jie","year":"2010","journal-title":"Open Pacing Electrophysiology Therapy Journal"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TBME.2006.876627"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_14"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0735-1097(02)01852-1"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1136\/heart.87.3.220"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780195058239.001.0001"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1136\/heart.89.8.939"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TBME.2003.808805"},{"key":"e_1_2_2_43_1","first-page":"17","article-title":"The pacemaker challenge: Developing certifiable medical devices (Dagstuhl seminar 14062)","volume":"4","author":"M\u00e9ry Dominique","year":"2014","journal-title":"Dagstuhl Reports"},{"key":"e_1_2_2_44_1","unstructured":"Dominique M\u00e9ry and Neeraj Kumar Singh. 2009. Pacemaker\u2019s Functional Behaviors in Event-B. Rapport de recherche. Retrieved from http:\/\/hal.inria.fr\/inria-00419973.  Dominique M\u00e9ry and Neeraj Kumar Singh. 2009. Pacemaker\u2019s Functional Behaviors in Event-B. Rapport de recherche. Retrieved from http:\/\/hal.inria.fr\/inria-00419973."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1111\/pace.12750"},{"key":"e_1_2_2_46_1","doi-asserted-by":"crossref","unstructured":"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.  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.","DOI":"10.1017\/S0007114510005441"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2012.25"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/TBME.1985.325532"},{"key":"e_1_2_2_49_1","first-page":"074","article-title":"Self-adjusting rate-responsive pacemaker and method thereof. Retrieved from https:\/\/www.google.co.uk\/patents\/US5074302","volume":"5","author":"Poore John W.","year":"1991","journal-title":"US Patent"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TBME.2007.897817"},{"key":"e_1_2_2_51_1","volume-title":"Handbook of Genetic Programming Applications","author":"Searson Dominic P."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02345444"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0735-1097(00)01054-8"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/SSIRI.2010.28"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.proeng.2011.08.331"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1540-8167.1989.tb01549.x"},{"key":"e_1_2_2_57_1","volume-title":"Proceedings of the 3rd International Conference on Computational Methods in Systems Biology","volume":"5","author":"Ye Pei"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220880.3220972"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3152767","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3152767","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3152767","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:09Z","timestamp":1750212669000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3152767"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8,9]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,10,31]]}},"alternative-id":["10.1145\/3152767"],"URL":"https:\/\/doi.org\/10.1145\/3152767","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,8,9]]},"assertion":[{"value":"2016-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-08-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}