Computational heart model
for clinical left atrium
arrhythmia ablation

Fiber effect
on activation patterns

Fiber's cancellation effect

Arrhythmia simulations

Fiber's effect
on rotor arrhythmias

Voltage threshold for
determing scar regions
in atrial fibrillation maps

Arrhythmia source detection

Heart model validation
with patient data

Medical Devices
Software Design

From Verified Model
to Verified Code

Heart Modeling
for Closed-loop
Evaluation of Pacemakers

Let our heart catch the bugs
Before your heart does

Pacemaker Software
with heart models

Safety and efficacy performance
of the pacemaker
at model level



Low-cost platform
for pacemaker
Evaluation & research

Patient-specific electrophysiological heart model for assisting left atrium arrhythmia ablation

    Atrial arrhythmia can be categorized into tachycardia, flutter, and fibrillation. Atrial fibrillation is a prevalent heart disease that results in weak and irregular contractions of the atria. It affects millions people worldwide and contributes to hundreds of thousands deaths annually. Cardiac ablation is among the most successful treatment options, involving the use of radio frequency energy to kill diseased cells or create lesion lines that obstruct abnormal activation waves. During the procedure, catheters are inserted into the left atrium to map the atrium geometry and record endocardium electrograms that are then converted into electroanatomical maps to pinpoint the arrhythmia source locations.

    However, identifying these sources is challenging. The electrograms are asynchronous and can be susceptible to noise. The spatial distribution of sampling sites is non-uniform, which leads to inaccurate maps. Identifying arrhythmia source locations is not a trivial task. Therefore, an ablation procedure often lasts from 3 to 6 hours, and arrhythmia recurrence within 12 months after first ablation is around 50%.

    To address these challenges, we developed an integrated computational heart mode for clinical left atrium arrhythmia ablation. Our system takes in the left atrium geometry and electrograms, processes them to extract regional tissue properties, which are used to tune a heart model, creating a patient-specific whole-atrium model. With this model, we can simulate and detect arrhythmia sources, and provide ablation assistance. To build such a system, we investigated the fiber effects on atrial activation patterns. We developed a fast heart model tuning method which takes only a few seconds of computation time on a personal computer, enabling real-time assistance during the ablation procedure. We achieved high accuracy in simulating arrhythmias, which we validated on patient data.

1. Background knowledge

Some background knowledge of left atrium arrhythmia, catheter ablation surgery, and atrial arrhythmia ablation challenges.

2. Research overview

An overview of our research: our approach and contributions.                                         

3. Fiber effects on activation patterns

Myocardial fiber data is not available for clinical arrhythmia ablation. We would like to find a way to compensate for the lack of fiber data. To do that, we need to first learn the effects of fiber on activation patterns.

4. Electrophysiological heart modeling

Explain the heart model equations and their parameters, derive the discrete form the heart model equations for programming and GPU parallel computing, and show arrhythmia simulation examples.

5. Patient-specific heart model parameter tuning

Derive a method for tuning diffusion coefficients of the fiber-independent model.

6. Clinical data processing: atrium mesh and electrogram

Describe the tools, user interfaces, and algorithms we developed for processing clinical data.

7. Electroanatomical maps and arrhythmia source detection

Explain the various maps we developed for detecting arrhythmia source locations.

8. Left atrium model validation on patient data

We tested our model with 15 patient data, to show that our model is capable of accurately reproducing patient arrhythmias.

From Verified Models to Verified Code

Our objective is to develop the scientific foundation for modeling, verification, synthesis, testing and optimization of safe software for Medical Cyber-Physical Systems. We focus on the safety of medical devices with the patient-in-the-loop and ensure the device will never drive the patient into an unsafe state while providing effective therapy. Our group's long term goal is to advance the theory and tools for model-driven development of medical devices and physiological control systems, so code generated from verified models is safe and efficient with closed-loop operation of the patient.

Heart Modeling for Closed-loop Validation of Implantable Cardiac Devices

The safety and efficacy of the device should be evaluated in the closed-loop state space of the heart and the pacemaker. A heart model is developed at both model level and implementation level to close the loop for pacemaker evaluation during the whole model-based design process.

Model Checking of Pacemaker Software

The safety and efficacy of the model of pacemaker software are evaluated in closed-loop with heart models at different abstraction levels. Counter-Example-Guided Abstraction and Refinement (CEGAR) framework is used to choose the appropriate heart model which balances the coverage and the expressiveness.


Model-based Design Framework

A model-driven development toolchain automatically translates formally verified models, which represent over-approximations of the realistic models, into deterministic models which can interact with real controllers within realistic environments. The model translation process guarantees that the properties verified in the early stage were still satisfied, as the system model was refined. As the verified model is translated into executable code for physical implementation, it is validated using conformance testing procedures based on the initial system specification.

Computer-Aided Clinical Trials

Clinical trials remain the ultimate validation approach for medical devices. Clinical trials are costly and pose risks to patients involved. In this work, we use implantable cardioverter difibrillator as example to demonstrate the use of computer models can aid planning and execution of clinical trials. We developed computer models of the heart and vary their parameters to represent a large variety of heart conditions. The models can generate synthetic Electrogram (EGM) signals which are the inputs to the devices. We evaluated and compared the performance of device algorithms from two device manufacturers which matched the results of a real clinical trial.

Physiological Control Systems

We focus on closed-loop safety analysis of physiological control systems which include networked sensors and actuators for drug delivery with complex patient-in-loop dynamics. These systems include Patient Controlled Analgesic infusion pumps where the controller is responsible for releasing the programmed dosage of the drug to the patient, while ensuring the patient is safe. Currently, patient safety can not be guaranteed due to an insufficient understanding of the body's response to treatment and the high degree of parametric uncertainty and variability between patients. For automated closed-loop control, we must thus use continuous monitoring of the patient's vitals to determine the safety state they are in, and based on a conservative over-approximation of the patient's dynamics, release the adequate dosage.