Infusion Pump Analysis

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!




  • 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.