Estimation and Verification of Hybrid Heart Models for Personalised Medical and Wearable Devices

We are witnessing a huge growth in popularity of wearable and implantable devices equipped with sensors that are capable of monitoring a range of physiological processes and communicating the data to smartphones or to medical monitoring devices. Applications include not only medical diagnosis and treatment, but also biometric identification and 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 authentication 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 testing. In this paper, we focus on applications that exploit the unique characteristics of the heart rhythm. We introduce a hybrid automata model of the electrical conduction system of a human heart, adapted from Lian et al. [8], 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.