A formal approach for the design of a rate adaptive pacemaker for heart failure

Abstract

Heart Failure (HF) is a chronic disease where the heart fails to pump sufficiently to maintain the required blood flow around the body. Currently, there are several therapies to improve HF, such as b-blockers and direct pacing. However, all these therapies have side effects and may not be able to provide optimal treatments for patients. In patients with HF, reduced Heart Rate Variability (HRV) is observed. Respiratory Sinus Arrhythmia (RSA) is the natural modulation in heart rate which contributes to the majority of HRV. It is observed in all mammals, with respect to breathing, by which the heart beats faster during inspiration and slower during expiration. Although the fundamental reason for the existence of RSA is still debatable, recent studies show that RSA increases the efficiency of cardiac output. Hence, it gives rise to the hypothesis that restoring RSA could bring therapeutic benefits to the patients. Cardiovascular Implantable Electronic Devices (CIEDs), such as pacemakers, are designed to treat patients with arrhythmias, especially bradycardia. Pacemakers work by stimulating the heart when needed. Conventional rate-adaptive pacemakers focus on meeting metabolic needs during physical or emotional activities by changing the pacing rate when such activities are detected. Although such devices can restore the critical cardiac rhythms of the patients, they are not able to reinstate the natural occurring RSA to improve HF. This thesis paves the way to develop Cardiovascular Implantable Electronic Device (CIED)s that provide HRV to bring beneficial effects for the patients with HF by proposing a new digital device that we call as a RSA pacemaker. RSA pacemakers are a combination of dual chamber pacemakers that are capable of adapting their pacing rate based on the breathing rate. The RSA pacemaker enables sensing and pacing on both the ventricle and the atrium of the heart with the properties of a conventional DDD mode pacemaker, while it monitors the respiratory signal to perform the RSA modulation for HRV. For a device such as the RSA pacemaker, it is important to be able to model the timing requirements for the correct behavior. We use the model-based approach to verify this new device. The behaviors of the RSA pacemaker are modeled with Synchronous Discrete Timed Automata (SDTA), proposed in this thesis. SDTA models of RSA pacemakers are translated into a formal language called Promela. The safety properties are then formally verified using the SPIN model checker. Using discrete clocks in SDTA for timing properties improves the well-known scalability issue during the verification process compared to its counterpart models using Timed Automata (TA) where time is expressed as real valued-clocks. The benchmarks show that the translated model takes the maximum verification time of 120 seconds whereas the verification does not finish within 48 hours using the TA models. The verified SDTA models are also automatically translated into C for hardware implementation. The translated C is ported into the ATmega328p processor for an animal trial with HF sheep. The respiratory signal is sensed by direct coupling the sheep’s diaphragm and measuring its change in Electromyography (EMG). The results show that the new RSA pacemaker can provide the RSA pacing while maintaining the safety timing requirements of the DDD mode pacemaker.