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

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 Evaluation of Pacemakers

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.

Pacemaker Software Verification

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.

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.