Infusion Pump Analysis Project
The aim of this project is to analyze medical devices with a focus on modeling the interaction of human operators of these devices and the impact of operator mistakes upon the overall safety of the interaction. Our approach uses models of the device operation, the patient’s physiological state (controlled by the device) and the operator of the device. Thus far, we have considered three scenarios to guide our research:
- We have studied generic drug infusion pump incorporating models of the operator with the pharmacokinetic/pharmacodynamic (PK/PD) model of the drug’s transport in the body of the patient. The goal is to relate mistakes committed during the interaction with their outcomes in terms of the concentration of drug reaching the effect chamber in the PK/PD model. Operator mistakes are modeled using a mistake model that specifies the morphing of the interaction under the action of a user error.
A FORMATS 2011 paper describes the model and its analysis using bounded-model checking (BMC). A follow up work to this focusses on three commercial infusion pump interfaces with mistake models constructed for each of these interfaces.
- Our ongoing work concerns insulin infusion pumps using non-linear models of the insulin-glucose regulatory system in the human body. Our goal is to correlate common insulin infusion pump usage strategies and operator mistakes with outcomes for the patient.
- As a related effort, we are investigating Electronic Medical Records (EMRs), errors and data variations in these records. The goal is to investigate how medical decisions can be affected by the presence of errors arising from human data entry mistakes but also due to the inherent uncertainties in the physiological measurements.
- Our ultimate goal (dream?) is to move beyond verification and synthesize interfaces that can help the user avoid errors systematically. Unfortunately, we do not have general recipes to achieve this. However, we are attempting to provide solutions to specific types of errors (eg., mode confusion) in a well-defined class of interfaces.
We will post some of the models and data from our work thus far. If you need help with compilation of the code or understanding the model, please email Sriram Sankaranarayanan .
- BMC model checker source code and models from our FORMATS 2011 paper: tar.gz (requires Z3 SMT solver to run. )
- Model for PCA + Continuous mode infusion process: click here .
- Simulink/Stateflow models coming soon.
Here is the progress we have made thus far!
- Paul Givens, Aleksandar Chakarov, Sriram Sankaranaryanan and Tom Yeh. Exploring the Internal State of User Interfaces by Combining Computer Vision Techniques with Grammatical Inference . 2012. Intl. Conference on Software Engg. (ICSE) New Ideas and Emerging Results (NIER) track, 2013 (to appear)
- Sriram Sankaranarayanan, Chris Miller, Rangarajan Ragunathan, Hadi Ravanbakhsh and Georgios Fainekos. A Model-Based Approach to Synthesizing Insulin Infusion Pump Usage Parameters for Diabetic Patients. Allerton 2012 conference proceedings , 2012 (invited paper ).
- Sriram Sankaranarayanan and Georgios Fainekos. Simulating Insulin Infusion Pump Risks by In-Silico Modeling of the Insulin-Glucose Regulatory System. Computational Methods in Systems Biology (CMSB) 2012, Vol 7605 of Lecture Notes in Computer Science, pp. 320 – 339 .
- Sriram Sankaranarayanan, Hadjar Homaei and Clayton Lewis. Model-Based Dependability Analysis of Programmable Real-Time Medical Devices , FORMATS 2011, Vol. 6919 of Lecture Notes in Computer Science, pp. 317-334.
- Sriram Sankaranarayanan and Georgios Fainekos. Falsification of Temporal Properties of Hybrid Systems using the Cross-Entropy Method , HSCC 2012, ACM Press, pp. 125–134.
- Prof. Sriram Sankaranarayanan (PI)
- Prof. Clayton Lewis (co-PI)
- Aleksandar Chakarov (PhD, CSCI)
- Nathan Lapinski (UG, CSCI)
- Paul Givens (UG, CSCI)
- Hadjar Homaei (MS CSCI)
- Sidartha Savio Flores Gracias (MS CSCI)
- Aaron Schlicht (ME CSCI)
This material is based upon work supported by the National Science Foundation (NSF) grant under the Cyber-Physical Systems (CPS) program award no. 1035845. All opinions expressed herein are those of the authors and not necessarily those of the NSF or the University of Colorado, Boulder.