Oxford logo
[CDKM13] T. Chen, M. Diciolla, M. Kwiatkowska and A. Mereacre. A Simulink Hybrid Heart Model for Quantitative Verification of Cardiac Pacemakers. In Proc. 16th International Conference on Hybrid Systems: Computation and Control (HSCC 2013), pages 131-136, ACM. 2013. [pdf] [bib]
Downloads:  pdf pdf (1.3 MB)  bib bib
Notes: Details of the models are here.
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.