From Verified Model
to Verified Code
Let our heart catch the bugs
Before your heart does
Safety and efficacy performance
of the pacemaker
at model level
Low-cost platform
for pacemaker
Evaluation & research
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.
Some background knowledge of left atrium arrhythmia, catheter ablation surgery, and atrial arrhythmia ablation challenges.
An overview of our research: our approach and contributions.
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.
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.
Derive a method for tuning diffusion coefficients of the fiber-independent model.
Describe the tools, user interfaces, and algorithms we developed for processing clinical data.
Explain the various maps we developed for detecting arrhythmia source locations.
We tested our model with 15 patient data, to show that our model is capable of accurately reproducing patient arrhythmias.
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.
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.
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.
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.
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.
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.
© mLab.Upenn. ALL Rights Reserved.
