Estimation and Verification of Hybrid Heart Models for

Abstract. We are witnessing a huge growth in popularity of wearable and implantable devices equipped with sensors that are capable of moni-toring a range of physiological processes and communicating the data to smartphones or to medical monitoring devices. Examples include fitness bands that can monitor the heartbeat and estimate the time you spend in deep sleep, wristbands that authenticate users based on the unique shape of their electrocardiogram (ECG), implantable glucose sensors that send measurements to an insulin pump, and leadless cardiac pacemakers that are implanted inside the heart. Applications include not only medical diagnosis and treatment, but also biometric authentication systems. An important requirement is personalisation of the devices, namely, their ability to adapt to the physiology of the human wearer and to faithfully reproduce the characteristics in real-time for the purposes of authentica-tion or optimisation of medical therapies. In view of the complexity of the embedded software that controls such devices, model-based frameworks have been advocated for their design, development, verification and test-ing. In this paper, we focus on applications that exploit the unique char-acteristics of the heart rhythm. We introduce a hybrid automata model of the electrical conduction system of a human heart, adapted from Lian et al [22], and present a framework for the estimation of personalised parameters, including the generation of synthetic ECGs from the model. We demonstrate the usefulness of the framework on two applications, ensuring safety of a pacemaker against a personalised heart model and ECG-based user authentication. The paper concludes by discussing the challenges and opportunities in this field.