Life-Critical Medical Devices: the Pacemaker

Objectives: Finite and Timed automata, appreciating the utility and challenges of formal proofs.

Tools: UPPAAL, Simulink
Models: Timed automata, deterministic automata, Partial Differential Equations.

Life-saving medical devices, like pacemakers and defibrillators, require a rigorous approach to verifying their safety. Testing, in which the device is fed different inputs and its behavior observed, cannot guarantee correctness and freedom from faults. Formal verification, on the other hand, provides such a guarantee.

In this project, I provide an overview of the fascinating computer models of the human heart out there, and get a feel for their capabilities. Then I will focus on timed automata, which allow us to formally and rigorously prove freedom from faults. 

Problem Statement:  Why Cardiac Modeling

Cardiac disease is the leading cause of death in the US • Around the world, 17.5 million people die of Cardiovascular Diseases (CVD) yearly • That’s an estimated 31% of all deaths • More than 75% of CVD deaths occur in low income and middle income countries • Implanted devices are a leading method of treating some CVDs

The consequences of incorrect algorithms and implementations are lethal.

Project Description - Modeling the Heart

We want to model the heart so that we can guarantee control with a pacemaker. In the heart model, the inputs are the pacing events generated by the pacemaker ( A_pace and V_pace ). The outputs are to predict whether there is beat in the Atrium (A_sense) and/or Ventricle (V_sense). There are two outputs because the pacemaker only measures electrical activity in two locations: the right atrium and the right ventricle. The pacemaker should be able to detect when the heart misses a beat and provide the appropriate pacing. Modeling can be achieved at various levels of abstraction. Examples of the possible abstraction levels in modeling the heart could be the following: whole heart, a ``slab of tissue'', a particular heart muscle cell (myocyte), or at the molecular level.

Electrical Activity

Automaton:  A machine that performs a function according to a predetermined set of coded instructions, especially one capable of a range of programmed responses to different circumstances.

Finite Automaton:  It is an abstract machine that can be in exactly one of a finite number of states at any given time.

Timed Automaton:  A finite automaton that has a notion of time or "clocks".  It is the node automaton and encompasses clocks, resets and actions.  A finite automaton extended with a finite set of real-valued clocks. During a run of a timed automaton, clock values increase all with the same speed. Along the transitions of the automaton, clock values can be compared to integers. These comparisons form guards that may enable or disable transitions and by doing so constrain the possible behaviors of the automaton.

Inputs:

• the pacing events generated by the pacemaker ( A_pace and V_pace )

Outputs:

• to predict whether there is beat in the Atrium (A_sense) and/or Ventricle (V_sense)

Problem Statement:

From 1990 to 2000, manufacturers recalled more than 600,000 cardiac medical devices. About 200,000 of those recalls were due to software problems.

With a typical pacemaker containing 80,000 to 100,000 lines of code, it is difficult for manufacturers to identify software errors using current industry practices. These practices rely on open-loop testing in which testers feed prerecorded heart signals to the pacemaker and evaluate the corresponding output. Open-loop testing can reveal how the pacemaker responds to various heart conditions, but not how the heart responds to the pacemaker in a closed-loop system. This is especially important in conditions such as pacemaker-mediated tachycardia, where the pacemaker can drive the heart into unsafe states.

Project Description:

Our team has developed a electrophysiological model of the heart that enables real-time closed-loop testing of pacemakers. 

We developed a simple and effective MATLAB/Simulink heterogeneous oscillator heart model capable to simulate the effect of external electrical signals on cardiac rhythm dynamics.

Using this model we observed reversible and irreversible conduction blocks as well as atrial and ventricular fibrillations under applications of an AC signals with different amplitude, frequency and duration to the natural pacemakers and cardiac muscles, respectively.

How Pacemakers Work

From one engineering perspective, the heart is a mechanical pump that circulates blood throughout the body. From the perspective of a pacemaker, it is a real-time system requiring precise timing of electrical signals.

The cardiac conduction system is a network of nodes and pathways carrying electrical signals that cause the chambers in the heart to contract and relax (Figure 1). In a healthy heart, contractions happen in rhythm. Disruptions in the cardiac conduction system can cause fast heartbeats—including atrial flutter and fibrillation—as well as slow heartbeats, known as bradycardia.

Figure 1. The electrical conduction system of the heart (left), represented as a network of nodes and pathways (right).

Pacemakers are fitted with electrodes that sense the heart’s electrical activity. When the pacemaker software detects an abnormal heart rhythm, it sends precisely timed electrical pulses to one or more of the heart’s chambers. The heart and pacemaker form a closed-loop system in which changes in the heart’s behavior lead to changes in pacemaker activity, and vice versa.

Modeling Nodes

Modeling AtoV Path

Normal Sinus Rhythem

Parameters: 60bpm, 150ms conduction delay between the atrium and ventricles

Modeling the Sinus Bradycardia

During Sinus Bradycardia, the SA node is not able to generate electrical events fast enough.

Modeling the Sinus Tachycardia

SA node generate frequent atrial events so that the heart rate is around 120bpm

Modeling the Atrio-Ventricular (AV) Block

The AV node blocks fast atrial events so that the corresponding ventricular rate remains within a normal range.  The AV node is blocking 1 out of every 2 atrial beats, thus keeping a 2:1 ratio between atria and ventricles.

Modeling AV Delay

PACEMAKER MODEL

Modeling Observance of VVI Pacemaker

Debuccing the VVI

Maintaining the Minimum Heart Rate