Closed-Loop Quantitative Verification of Rate-Adaptive Pacemakers

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.