Quantitative Regular Expressions for Arrhythmia Detection.

Implantable medical devices are safety-critical systems whose incorrect operation can jeopardize a patient's health, and whose algorithms must meet tight platform constraints like memory consumption and runtime. In particular, we consider here the case of implantable cardioverter defibrillators, where peak detection algorithms and various others discrimination algorithms serve to distinguish fatal from non-fatal arrhythmias in a cardiac signal. Motivated by the need for powerful formal methods to reason about the performance of arrhythmia detection algorithms, we show how to specify all these algorithms using Quantitative Regular Expressions (QREs). QRE is a formal language to express complex numerical queries over data streams, with provable runtime and memory consumption guarantees. We show that QREs are more suitable than classical temporal logics to express in a concise and easy way a range of peak detectors (in both the time and wavelet domains) and various discriminators at the heart of today's arrhythmia detection devices. The proposed formalization also opens the way to formal analysis and rigorous testing of these detectors' correctness and performance, alleviating the regulatory burden on device developers when modifying their algorithms. We demonstrate the effectiveness of our approach by executing QRE-based monitors on real patient data on which they yield results on par with the results reported in the medical literature.

Computer Aided Clinical Trials for Implantaule Cardiac Devices.

In this paper we aim to answer the question, "How can modeling and simulation of physiological systems be used to evaluate life-critical implantable medical devices?" Clinical trials for medical devices are becoming increasingly inefficient as they take several years to conduct, at very high cost and suffer from high rates of failure. For example, the Rhythm ID Goes Head-to-head Trial (RIGHT) sought to evaluate the performance of two arrhythmia discriminator algorithms for implantable cardioverter defibrillators, Vitality 2 vs. Medtronic, in terms of time-to-first inappropriate therapy, but concluded with results contrary to the initial hypothesis- after 5 years, 2,000+ patients and at considerble ethical and monetary cost. In this paper, we describe the design and performance of a Computer-aided Clinical Trial (CACT) for Implantable Cardiac Devices where previous trial information, real patient data and closed-loop device models are effectively used to evaluate the trial with high confidence. We formulate the CACT in the context of RIGHT using a Bayesian statistical framework. We define a hierarchical model of the virtual cohort generated from a physiological model which captures the uncertainty in the parameters and allow for the systematic incorporation of information available at the design of the trial. With this formulation, the estimates the inappropriate therapy rate of Vitality 2 compared to Medtronic as 33.22% vs 15.62% $(\mathrm{p}\lt 0.001)$, which is comparable to the original trial. Finally, we relate the outcomes of the computer- aided clinical trial to the primary endpoint of RIGHT.

In-silico pre-clinical trials for implantable cardioverter defibrillators.

Regulatory authorities require that the safety and efficacy of a new high-risk medical device be proven in a Clinical Trial (CT), in which the effects of the device on a group of patients are compared to the effects of the current standard of care. Phase III trials can run for several years, cost millions of dollars, and expose patients to an unproven device. In this paper, we demonstrate how to use a large group of synthetic patients based on computer modeling to improve the planning of a CT so as to increase the chances of a successful trial for implantable cardioverter defibrillators (ICDs). We developed a computer model of the electrical generation and propagation in the heart. This model was used to generate a large group of heart instances capable of producing episodes of 19 different arrhythmias. We also implemented two arrhythmia detection algorithms from the literature: Rhythm ID from Boston Scientific and PR Logic + Wavelet from Medtronic. Using this setup, we conducted multiple in-silico trials to compare the ability of the two algorithms to appropriately discriminate between potentially fatal Ventricular Tachy-arrhythmias (VT) and nonfatal Supra-Ventricular Tachy-arrhythmias (SVTs). The results of our in-silico trial indicate that Rhythm ID was less able to discriminate between SVT and VT and so may lead to more cases of inappropriate therapy. This corroborates the findings of the Rhythm ID Going Head to Head Trial (RIGHT), a clinical trial that compared the two algorithms in patients. We further demonstrated that the result continues to hold if we vary the distribution of arrhythmias in the synthetic population. We also used the same in-silico cohort to explore the sensitivity of the outcome to different parameter settings of the device algorithms, which is not feasible in a real clinical trial. In-silico trials can provide early insight into the factors which affect the outcome of a CT at a fraction of the cost and duration and without the ethical issues.