Simulating insulin infusion pump risks by In-Silico modeling of the insulin-glucose regulatory system

Abstract. We present a case study on the use of robustness-guided and statistical model checking approaches for simulating risks due to insulin infusion pump us-age by diabetic patients. Insulin infusion pumps allow for a continuous delivery of insulin with varying rates and delivery profiles to help patients self-regulate their blood glucose levels. However, the use of infusion pumps and continuous glucose monitors can pose risks to the patient including chronically elevated blood glu-cose levels (hyperglycemia) or dangerously low glucose levels (hypoglycemia). In this paper, we use mathematical models of the basic insulin-glucose regula-tory system in a diabetic patient, insulin infusion pumps, and the user’s interac-tion with these pumps defined by commonly used insulin infusion strategies for maintaining normal glucose levels. These strategies include common guidelines taught to patients by physicians and certified diabetes educators and have been implemented in commercially available insulin bolus calculators. Furthermore, we model the failures in the devices themselves along with common errors in the usage of the pump. We compose these models together and analyze them using two related techniques: (a) robustness guided state-space search to explore worst-case scenarios and (b) statistical model checking techniques to assess the proba-bilities of hyper- and hypoglycemia risks. Our technique can be used to identify the worst-case effects of the combination of many different kinds of failures and place high confidence bounds on their probabilities.