Artificial Pancreas (AP) Verification Project
Welcome to the project page for the artificial pancreas project. This project is a collaboration between engineers, computer scientists, mathematicians, and clinical researchers centered around the mathematical modeling, simulation and formal analysis of the artificial pancreas concept.
What is the Artificial Pancreas?
The artificial pancreas is a concept that involves the development of a series of increasingly sophisticated “Cyber-Physical Systems” that will automate the delivery of insulin to people with Type-1 Diabetes.
Warning: this is a simple (possibly simplistic) explanation that omits many key details. It is suitable as an overview and not intended to be a clinical presentation. The interested reader should consult a book (We recommend the Pink Panther book by Drs. Chase and Maahs).
What is Type-1 Diabetes?
Type-1 Diabetes (T1D) is a serious condition caused by the inability or the decreased ability of the pancreas to secrete insulin. This can happen due to numerous reasons: for example, as a result of an autoimmune response that destroys the beta cells of the pancreas; or as a result of certain surgical procedures. Insulin is an important hormone that is responsible for regulating the uptake of Glucose by various cells in the body causing the lowering of blood glucose levels. Lack of insulin leads to increased blood glucose levels. However, the glucose in the blood is not taken up by the cells that convert them to energy or store them. As a result, the cells are starved of much needed energy and this results in their breakdown.
Currently, T1D is treated through the external administration of artificial insulin analogs either through daily injections or an insulin infusion pump. The latter option is increasingly popular with patients, since it provides substantial freedom in their choice of meals, exercise and other activities that affect their metabolism. The infusion pumps are operated manually by the patient based on their anticipated mealtimes, meal carbohydrate amounts and exercise times/intensities. The infusion pumps currently available in the market can deliver short acting insulin analogs at programmable doses, all day and night. This typically involves a background “basal” delivery of insulin and numerous boluses delivered at mealtimes. Manual control of pump has two main drawbacks:
- It imposes the burden of managing the blood glucose levels on the patients. Typically this involves roughly 6-9 blood glucose measurements, basal adjustments and bolus infusions throughout the day.
- Failure to maintain blood glucose levels inside the euglycemic range [70,170] mg/dl can have serious consequences. If too much insulin is infused, it can drive the blood glucose levels dangerously low, causing hypoglycemia. If too little is infused, it can cause high blood gluocse levels with short term (ketacidosis) and long term consequences (damage to kidneys, heart, nerves and eyes).
The Artificial Pancreas
The artificial pancreas (AP) is a series of increasingly sophisticated devices that will increasingly automate insulin delivery to the patient. It has been enabled by insulin infusion pumps that can deliver insulin automatically and be programmed externally by a software-based controller. On the other hand, glucose sensor technology has developed sufficiently to provide accurate, near realtime subcutaneous glucose measurement. Many stages have been envisioned for the AP, and the technological feasibility of each stage has been demonstrated in clinical trials. The original stages of the AP were proposed by the JDRF as follows:
- Pump shutoff: this stage simply shuts down the pump and alarms when the blood glucose is too low. This technology has already been useful at nighttimes to alert patients and their care providers when the blood glucose level drops.
- Predictive Pump shutoff: this device forecasts the near term future glucose trend form the current observed glucose values. If the forecast calls for a low in the next 30-70 minutes, the pump is shutoff in anticipation of the low and turned back on as soon as the glucose levels rise.
- Hybrid Closed Loop: This stage controls the basal insulin delivery, relying on daytime boluses by the user.
- Fully automatic closed loop: This stage controls both basal delivery and automatic meal boluses.
- Multihormone closed loop: This stage uses multiple hormones instead of just insulin. Specifically, glucagon (the counterregulatory hormone to insulin) is also used to increase blood glucose levels and in some designs, amylin is added to control the digestion of food.
Recently, it has been noted that all stages have been implemented and proven to be technologically viable in various stages of clinical trials. A simpler classification has been proposed by the JDRF as (a) daytime vs. nighttime-only control and (b) insulin-only vs. multi-hormonal control.
Formal Verificationoject proposes to verify AP control systems to find possible issues with these systems before deployment.
What is formal verification?
Engineered systems are often prone to design faults that arise due to numerous reasons, including design and implementation mistakes. These are particularly problematic with software systems that tend to be designed by a large team of people. Verification is the process by which, these devices are tested and known defects that arise are fixed. However, manual verification is expensive and prone to errors, as well. Therefore, formal verification techniques try to automate the verification process to provide more guarantees at the end of the verification. Ideally, these are exhaustive techniques that either provide a mathematical proof that the system is correct or expose a bug/defect in the design.
However, there are fundamental reasons why fully exhaustive and automated verification of software systems is a really hard problem, if not downright impossible! Nevertheless, we have been trying many partial solutions that have yielded varying degrees of success: these solutions focus on solving the problem for special classes of systems or abstracting the system model into a special form before reasoning about them.
Why verify the Artificial Pancreas?
The artificial pancreas is safety critical. Ultimately, it takes autonomy away from patients with T1D in return for a reduced burden of diabetes management. It is essential that the control software be free of common software bugs such a buffer overflows, division by zero, and memory leaks. However, the AP is not just software: it includes physical components like sensors, pumps and an entire human body in the loop! As such, it has to deal with a large set of uncertainties in it’s operation. Examples include unannounced meals, exercise, sensor noise, erroneous sensor readings, pressure induced sensor attenuation, set failures, and patient physiological changes. Besides software bugs, we need to exhaustively run our designs through billions of scenarios to see if the system behaves “reasonably” in all scenarios. Worst of all, we need a good definition of what “reasonable” is.
Aren’t Clinical Trials Good Enough?
Clinical trials differ widely in what they study and how they study. The answer below is not truly representative of all possible studies that have been carried out for AP controllers
In some sense, clinical trials will be “good enough” when the technology is deployed to a large population of users and tested for a long time under varying conditions. Otherwise, most trials are not meant to test for the “worst case”. Worst case effects are by definition rare and only seen when a product is deployed.
What stops us from verifying AP controllers?
As mentioned earlier, verification is a very hard problem. We have billions, if not trillions, of scenarios to run through and test. It is hard to go through each one by one. As a result, mathematical models should be used by engineers to capture processes like the human insulin-glucose response, the patterns of sensor noise, set failures and other disturbances. There has been a lot of work on simulating AP controllers. In fact, some models like the Dalla-Man et al. model have been used with FDA’s encouragement as a stand in for animal trials of AP controllers. However, these models are nonlinear and as such, many verification tools that exist cannot handle these models or can be very slow. However, we are making progress on tools like S-Taliro, Flow* and dReal, that can perform restricted forms of automated verification for nonlinear dynamics.
To conclude, a significant gap needs to be bridged between what formal tools can do currently, and what is needed to automate an exhaustive analysis of AP controllers.
Project Goalsgoal of this project is to provide a focussed effort around developing formal tools for verifying artificial pancreas controllers. The project has multiple thrusts including:
- Developing disturbance models for meal, exercise, sensor noise, dropouts, set failures and other disturbances.
- Developing simpler, perhaps even nondeterminstic models, of insulin-glucose response. We are looking into delay differential models and nondeterministic “minimal models” built using the available data.
- Developing formal verification tools for nonlinear dynamics so that they can reason about controller implementations and nonlinear dynamics models.
- Developing a set of properties that need to be verified.
- Case-studies on real-life systems that have been deployed in clinical trials.
- Focus on presentation of results to engineers and clinicians to better understand the root cause of defects and judge their real-life feasibility.
Project Teaminvolves a mutidisciplinary team of computer scientists, chemical engineers, mathematicians and clinical researchers from multiple institutions.
- Fraser Cameron (joint PI), Mechanical Engg., University of Texas, El Paso.
- Sriram Sankaranarayanan (joint PI), Computer Science, CU Boulder.
- David Maahs (joint PI), Pediatric Endocrinology, Barbara Davis Center for Childhood Diabetes, UC Denver Medical School.
- B. Wayne Bequette (senior person), Chemical Engg., RPI.
- David Bortz (co-PI), Applied Mathematics, CU Boulder.
- Shalom Ruben (co-PI), Mechanical Engg., CU Boulder.
- Suhas Akshar Kumar (MS, Electrical Engg.), CU Boulder.
- Tasia Kushner (PhD, IQ Biology), CU Boulder.
- Alexandra Okeson (BS, Computer Science), CU Boulder.
- Greg Forlenza, Pediatric Endocrinology, Barbara Davis Center for Childhood Diabetes, UC Denver Medical School.
PublicationPublicationP Forlenza, Sriram Sankaranarayanan, and David M Maahs, Refining the Closed Loop in the Data Age: Research-to-Practice Transitions in Diabetes Technology (Editorial) In Diabetes Technology and Therapeutics Vol. 17(5), pp. 304-306 (2015) .
Fundingfunded by the US National Science Foundation (NSF) under awards CPS-1446900 and CPS-1446751. All opinions expressed here are those of the authors and not necessarily of the US National Science Foundation (NSF).