Project Page for Artificial Pancreas Verification Project
This page describes ongoing collaborative research funded 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).
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. 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.
Background on 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.
The formal verification project 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 its 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?
Note: 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.
The basic goal of this project is to provide a focused effort around developing formal tools for verifying artificial pancreas controllers. The project has multiple thrusts including:
The project involves a mutidisciplinary team of computer scientists, chemical engineers, mathematicians and clinical researchers from multiple institutions.
Postdoctoral Research Associate
Sriram Sankaranarayanan, Suhas Akshar Kumar, Faye Cameron, B. Wayne Bequette, Georgios Fainekos, and David M. Maahs, Model-Based Falsification of an Artificial Pancreas Control System. In ACM SIGBED Review (Special Issue on Medical Cyber Physical Systems) Vol. TBA, pp. TBA (2016). Note: Presented at MEDCPS Workshop 2016
Gregory P. 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).
Fraser Cameron, Georgios Fainekos, David M. Maahs, and Sriram Sankaranarayanan, Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification In Proceedings of Runtime Verification (RV'15), Volume 9333 of Lecture Notes in Computer Science pp. 3-17 (2015). Note: Invited Keynote Paper
Stephen M. Kissler, Cody Cichowitz, Sriram Sankaranarayanan, and David M. Bortz, Determination of personalized diabetes treatment plans using a two-delay model In J. Theoretical Biology Vol. 359(Oct), pp. 101-111 (2014).
This page was authored and maintained by Sriram Sankaranarayanan, who is responsible for its content. Please direct all queries to Sriram at his email address