A Simulink Hybrid Heart Model for Quantitative Verification of Cardiac Pacemakers

Abstract

We 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 stochasticity. It is inspired by the timed and hybrid automata network models of Jiang et al and Ye et al, where probabilistic behaviour is not considered. In contrast to our earlier work, we work directly with action potential signals that the pacemaker sensor inputs from a specific cell, rather than ECG signals. We validate the model by demonstrating that its composition with a pacemaker model can be used to check safety properties by means of approximate probabilistic verification.