Note: Work on this particular NSF project concluded in 2019. We will post details of our current work on artificial pancreas devices soon.
This page describes 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
What follows below 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. I 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:
. 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. . Last but not least, Develop ways to present verification results to engineers and clinicians to better understand the root cause of defects and judge their real-life feasibility.
The project involves a mutidisciplinary team of computer scientists, chemical engineers, mathematicians and clinical researchers from multiple institutions.
- Faye Cameron (joint PI), Chemical Engg. RPI.
- 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.
- Taisa Kushner (PhD, IQ Biology), CU Boulder.
- Suhas Akshar Kumar
- Ram Das Diwakaran
- Alexandra Okeson
- Dr. Xin Chen
- Greg Forlenza, MD, Pediatric Endocrinology, Barbara Davis Center for Childhood Diabetes, UC Denver Medical School.
- Laurel Messer, PhD, School of Nursing and Barbara Davis Center for Childhood Diabetes, UC Denver Medical School.
- Weighted Transducers for Robustness VerificationIn Intl. Conference on Concurrency Theory (CONCUR), pp. 17:1–17:21, 2020.
- Multi-hour Blood Glucose Prediction in T1D: A Patient Specific Approach using Shallow Neural Network ModelsDiabetes Technology and Therapeutics, 22 (12) pp. 883-891, 2020.
- Conformance verification for neural network models of glucose-insulin dynamicsIn Hybrid Systems: Computation and Control (HSCC), pp. 13:1–13:12, 2020.
- Models, Devices, Properties and Verification of Artificial Pancreas SystemsIn Automated Reasoning for Systems Biology And Medicine (Edited by Paulo Zuliani and Pietro Lio), pp. 93-131, 2019.
- Factory-Calibrated Continuous Glucose Monitoring: How and Why It Works, and the Dangers of Reuse Beyond Approved Duration of WearDiabetes: Technology and Therapeutics, 21 (4) pp. 222-229, 2019.Note: Peer-Reviewed Commentary..
- Robust Data-Driven Control of Artificial Pancreas Systems using Neural NetworksIn Computational Methods in Systems Biology, Lecture Notes In Computer Science Vol. 11095, pp. 183-202, 2018.
- A Data-Driven Approach to Artificial Pancreas Verification and Synthesis.In Intl. Conference on Cyber-Physical Systems (ICCPS’18), pp. 242-252, 2018.
- Compositional Relational Abstraction for Nonlinear SystemsACM Transactions on Embedded Computing Systems (Special Issue for EMSOFT 2017), 16(5s) pp. 187, 2017.Note: EMSOFT 2017 Best Paper Award Nomination.
- Formal Verification of a Multi-Basal Insulin Infusion Control Model.In Workshop on Applied Verification of Hybrid Systems (ARCH), pp. 16, 2017.
- Analyzing Neighborhoods of Falsifying Traces in Cyber-Physical SystemsIn Intl. Conference on Cyber-Physical Systems (ICCPS), pp. 109-119, 2017.
- Model-Based Falsification of an Artificial Pancreas Control System.ACM SIGBED Review (Special Issue on Medical Cyber Physical Systems) , 14 (2) pp. 24-33, 2016.Note: Presented at MEDCPS Workshop 2016.
- Refining the Closed Loop in the Data Age: Research-to-Practice Transitions in Diabetes Technology (Editorial)Diabetes Technology and Therapeutics, 17 (5) pp. 304-306, 2015.
- Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime VerificationIn Proceedings of Runtime Verification (RV’15), Lecture Notes in Computer Science Vol. 9333, pp. 3-17, 2015.Note: Invited Keynote Paper.
- Determination of personalized diabetes treatment plans using a two-delay modelJ. Theoretical Biology, 359 (Oct) pp. 101-111, 2014.
- The Flow* tool and S-Taliro tool have been used so far to verify the artificial pancreas control algorithms.
- Course on Closed Loop Medical Devices at CU Boulder.
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.