Formal Modelling and Validation of Rate-Adaptive Pacemakers

Rate-adaptive pacemakers make use of sensors in order to automatically adjust the pacing rate according to the metabolic needs of the patient, thus overcoming the limitation of fixed-rate pacemakers that cannot ensure an adequate heart beat in cases of varying physical, mental or emotional activity. This feature significantly improves the quality of life of patients with chronotropic incompetence, i.e. Whose heart is unable to increase its rate as the activity increases. We develop a formal model of a rate-adaptive pacemaker based on hybrid automata that explicitly includes sensors for rate control. In particular, we model the VVIR pacemaker with a QT interval sensor, a highly specific metabolic sensor that can sense the exercise activity level, based on the fact that physical (and mental) stresses shorten the QT interval, in turn requiring an increased heart rate. We implement the QT interval sensor through a runtime ECG detection algorithm and validate our model with patient data, showing that the simulated VVIR pacemaker is able to successfully regulate a bradycardia ECG signal and produce a correctly paced heart. The validated rate-adaptive pacemaker is plugged into the model-based framework introduced in Chen et al. (2014), which enables rigorous and quantitative verification of closed-loop patient-device systems described as hybrid automata, and supports multiple heart and pacemaker models in a modular way. We demonstrate the usefulness of the framework by performing in silico experiments to demonstrate the correct functioning of rate modulation under different activity levels. Our framework has the potential to reduce the need for exercise testing with real patients.