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
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.
2014 © mLab.Upenn. ALL Rights Reserved.
