Artificial Pancreas Verification Project

Automata theory provides us with fundamental notions such as languages, membership, emptiness and inclusion that in turn allow us to specify and verify properties of reactive systems in a useful manner. However, these notions all yield "yes"/"no" answers that sometimes fall short of being satisfactory answers when the models being analyzed are imperfect, and the observations made are prone to errors. As a result, a common engineering approach is not just to verify that a system satisfies a property, but it does so robustly. In this paper, we present notions of robustness that place a metric on words, thus providing a natural notion of distance between words. Such a metric naturally leads to a topological neighborhood of words and languages, leading to quantitative and robust versions of the membership, emptiness and inclusion problems. The main contribution of this work is to study such problems in the context of weighted transducers. We provide algorithms for solving the robust and quantitative versions of the membership and inclusion problems while providing useful motivating case studies including a modeling an error-prone human operator and approximate pattern matching in a large type-1 diabetes dataset.

Considering current insulin action profiles and the nature of glycemic responses to insulin, there is an acute need for longer-term, accurate, blood glucose predictions to inform insulin dosing schedules and enable effective decision support for the treatment of type 1 diabetes (T1D). However, current methods achieve acceptable accuracy only for prediction horizons of up to one hour, whereas typical post-prandial excursions and insulin action profiles last 4-6 hours. In this work, we present models for prediction horizons of 60-240min developed by leveraging “shallow” neural networks, allowing for significantly lower complexity when compared to related approaches. Methods: Patient-specific neural network-based predictive models are developed and tested on previously collected data from a cohort of twenty-four subjects with T1D. Models are designed to avoid serious pitfalls through incorporating essential physiological knowledge into model structure. Patient-specific models were generated to predict glucose 60, 90, 120, 180, and 240 minutes ahead, and a "transfer learning" approach to improve accuracy for patients where data is limited. Finally, we determined subgroup characteristics which result in higher model accuracy overall. Results: RMSE was 28+/- 4 mg/dL, 33+/-4 mg/dL, 38±6 mg/dL, 40+/-8 mg/dL, and 43+/-12mg/dL for 60, 90, 120, 180, and 240minutes respectively. For all prediction horizons, at least 93% of predictions were clinically acceptable by the Clarke Error Grid. Variance of historic continuous glucose monitor (CGM) values was a strong predictor for the need of transfer learning approaches. Conclusions: A shallow neural network, using features extracted from past CGM data and insulin logs is able to achieve multi-hour glucose predictions with satisfactory accuracy. Models are patient-specific, learned on readily-available data without the need for additional tests, and improve accuracy while lowering complexity when compared to related approaches, paving the way for new advisory and closed loop algorithms able to encompass most of the insulin action time-frame.

Neural networks present a useful framework for learning complex dynamics, and are increasingly being considered as components to closed loop predictive control algorithms. However, if they are to be utilized in such safety-critical advisory settings, they must be provably “conformant” to the governing scientific (biological, chemical, physical) laws which underlie the modeled process. Unfortunately, this is not easily guaranteed as neural network models are prone to learn patterns which are artifacts of the conditions under which the training data is collected, which may not necessarily conform to underlying physiological laws. In this work, we utilize a formal range-propagation based approach for checking whether neural network models for predicting future blood glucose levels of individuals with type-1 diabetes are monotonic in terms of their insulin inputs. These networks are increasingly part of closed loop predictive control algorithms for “artificial pancreas” devices which automate control of insulin delivery for individuals with type-1 diabetes. Our approach considers a key property that blood glucose levels must be monotonically decreasing with increasing insulin inputs to the model. Multiple representative neural network models for blood glucose prediction are trained and tested on real patient data, and conformance is tested through our verification approach. We observe that standard approaches to training networks result in models which violate the core relationship between insulin inputs and glucose levels, despite having high prediction accuracy. We propose an approach that can learn conformant models without much loss in accuracy.

In this chapter, we present the interplay between models of human physiology, closed loop medical devices, correctness specifications and verification algorithms in the context of the artificial pancreas. The artificial pancreas refers to a series of increasingly sophisticated closed loop medical devices that automate the delivery of insulin to people with type-1 diabetes. On one hand, they hold the promise of easing the everyday burden of managing type-1 diabetes. On the other, they expose the patient to potentially deadly consequences of incorrect insulin delivery that could lead to coma or even death in the short term, or damage to critical organs such as the eyes, kidneys and the heart in the longer term. Verifying the correctness of these devices involves a careful modeling of human physiology, the medical device, and the surrounding disturbances at the right level of abstraction. We first provide a brief overview of insulin glucose regulation and the spectrum of associated mathematical models. At one end are physiological models that try to capture the transport, metabolism, uptake and interactions of insulin and glucose. On the end are data driven models which include time series models and neural networks. The first part of the chapter examines some of these models in detail in order to provide a basis for verifying medical devices. Next, we present some of the devices which are commonly used in blood glucose control, followed by a specification of key correctness properties and performance measures. Finally, we examine the application of some of the state-of-the-art approaches to verification and falsification of these properties to the models and devices considered. We conclude with a brief presentation on future directions for next generation artificial pancreas, and the challenges involved in reasoning about them.

Continuous glucose monitors (CGM) display real-time glucose values enabling greater glycemic awareness with reduced management burden. Factory-calibrated CGM systems allow for glycemic assessment without the pain and inconvenience of fingerstick glucose testing. Advances in sensor chemistry and CGM algorithms have enabled factory-calibrated systems to have greater accuracy than previous generations of CGM technology. Despite these advances many patients and providers are hesitant about the idea of removing fingerstick testing from their diabetes care. In this commentary, we aim to review the clinical trials on factory-calibrated CGM systems, present the algorithms which facilitate factory-calibrated CGMs to improve accuracy, discuss clinical use of factory-calibrated CGMs, and finally present two cases demonstrating the dangers of utilizing exploits in commercial systems to prolong sensor life.

In this paper, we provide an approach to data-driven control for artificial pancreas system by learning neural network models of human insulin-glucose physiology from available patient data and using a mixed integer optimization approach to control blood glucose levels in real-time using the inferred models. First, our approach learns neural networks to predict the future blood glucose values from given data on insulin infusion and their resulting effects on blood glucose levels. However, to provide guarantees on the resulting model, we use quantile regression to fit multiple neural networks that predict upper and lower quantiles of the future blood glucose levels, in addition to the mean. Using the inferred set of neural networks, we formulate a model-predictive control scheme that adjusts both basal and bolus insulin delivery to ensure that the risk of harmful hypoglycemia and hyperglycemia are bounded using the quantile models while the mean prediction stays as close as possible to the desired target. We discuss how this scheme can handle disturbances from large unannounced meals as well as infeasibilities that result from situations where the uncertainties in future glucose predictions are too high. We experimentally evaluate this approach on data obtained from a set of 17 patients over a course of 40 nights per patient. Furthermore, we also test our approach using neural networks obtained from virtual patient models available through the UVA-Padova simulator for type-1 diabetes.

This paper presents a case study of a data driven approach to verification and parameter synthesis for artificial pancreas control systems which deliver insulin to patients with type-1 diabetes (T1D). We present a new approach to tuning parameters using non-deterministic data-driven models for human insulin-glucose regulation, which are inferred from patient data using multiple time scales. Taking these equations as constraints, we model the behavior of the entire closed loop system over a five-hour time horizon cast as an optimization problem. Next, we demonstrate this approach using patient data gathered from a previously conducted outpatient clinical study involving insulin and glucose data collected from 50 patients with T1D and 40 nights per patient. We use the resulting data-driven models to predict how the patients would perform under a PID-based closed loop system which forms the basis for the first commercially available hybrid closed loop device. Futhermore, we provide a re-tuning methodology which can potentially improve control for 82% of patients, based on the results of an exhaustive reachability analysis. Our results demonstrate that simple nondeterministic models allow us to efficiently tune key controller parameters, thus paving the way for interesting clinical translational applications.

We propose techniques to construct abstractions for nonlinear dynamics in terms of relations expressed in linear arithmetic. Such relations are useful for translating the closed loop verification problem of control software with continuous-time, nonlinear plant models into discrete and linear models that can be handled by efficient software verification approaches for discrete-time systems. We construct relations using Taylor model based flowpipe construction and the systematic composition of relational abstractions for smaller components. We focus on developing efficient schemes for the special case of composing abstractions for linear and nonlinear components. We implement our ideas using a relational abstraction system, using the resulting abstraction inside the verification tool NuXMV, which implements numerous SAT/SMT solver-based verification techniques for discrete systems. Finally, we evaluate the application of relational abstractions for verifying properties of time triggered controllers, comparing with the Flow* tool. We conclude that relational abstractions are a promising approach towards nonlinear hybrid system verification, capable of proving properties that are beyond the reach of tools such as Flow*. At the same time, we highlight the need for improvements to existing linear arithmetic SAT/SMT solvers to better support reasoning with large relational abstractions.

The artificial pancreas concept automates the delivery of insulin to patients with type-1 diabetes, sensing the blood glucose levels through a continuous glucose monitor (CGM) and using an insulin infusion pump to deliver insulin. Formally verifying control algorithms against physiological models of the patient is an important challenge. In this paper, we present a case study of a simple hybrid multi-basal control system that switches to different preset insulin delivery rates over various ranges of blood glucose levels. We use the Dalla-Man model for modeling the physiology of the patient and a hybrid automaton model of the controller. First, we reduce the problem state space and replace nonpolynomial terms by approximations with very small errors in order to simplify the model. Nevertheless, the model still remains nonlinear with up to 9 state variables. Reachability analysis on this hybrid model is used to verify that the blood glucose levels remain within a safe range overnight. This poses challenges, including (a) the model exhibits many discrete jumps in a relatively small time interval, and (b) the entire time horizon corresponding to a full night is 720 minutes, wherein the controller time period is 5 minutes. To overcome these difficulties, we propose methods to effectively handle time-triggered jumps and merge flowpipes over the same time interval. The evaluation shows that the performance can be improved with the new techniques.

We study the problem of analyzing falsifying traces of cyber-physical systems. Specifically, given a system model and an input which is a counterexample to a property of interest, we wish to understand which parts of the inputs are “responsible” for the counterexample as a whole. Whereas this problem is well known to be hard to solve precisely, we provide an approach based on learning from repeated simulations of the system under test. Our approach generalizes the classic concept of “one-at-a-time” sensitivity analysis used in the risk and decision analysis community to understand how inputs to a system influence a property in question. Specifically, we pose the problem as one of finding a neighborhood of inputs that contains the falsifying counterexample in question, such that each point in this neighborhood corresponds to a falsifying input with a high probability. We use ideas from statistical hypothesis testing to infer and validate such neighborhoods from repeated simulations of the system under test. This approach not only helps to understand the sensitivity of these counterexamples to various parts of the inputs, but also generalizes or widens the given counterexample by returning a neighborhood of counterexamples around it. We demonstrate our approach on a series of increasingly complex examples from automotive and closed loop medical device domains. We also compare our approach against related techniques based on regression and machine learning.

We present a model-based falsification scheme for artificial pancreas controllers. Our approach performs a closed-loop simulation of the control software using models of the human insulin-glucose regulatory system. Our work focuses on testing properties of an overnight control system for hypoglycemia/hyperglycemia minimization in patients with type-1 diabetes. This control system is currently the subject of extensive phase II clinical trials. We describe how the overall closed loop simulator is constructed, and formulate properties to be tested. Significantly, the closed loop simulation incorporates the control software, as is, without any abstractions. Next, we demonstrate the use of a simulation-based falsification approach to find potential property violations in the resulting control system. We formulate a series of properties about the controller behavior and examine the violations obtained. Using these violations, we propose modifications to the controller software to improve its performance under these adverse (corner-case) scenarios. We also illustrate the effectiveness of robustness as a metric for identifying interesting property violations. Finally, we identify important open problems for future work.

The editorial analyzes a recent clinical study reporting on the impact of insulin pump shutoff on patients with type-1 diabetes. In a broader context, it examines the need for enhanced formal verification techniques applied to more sophisticated artificial pancreas controllers that remain under development.

In this paper, we briefly examine the recent developments in artificial pancreas controllers, that automate the delivery of insulin to patients with type-1 diabetes. We argue the need for offline and online runtime verification for these devices, and discuss challenges that make verification hard. Next, we examine a promising simulation-based falsification approach based on robustness semantics of temporal logics. These ideas are implemented in the tool S-Taliro that automatically searches for violations of metric temporal logic (MTL) requirements for Simulink(tm)/Stateflow(tm) models. We illustrate the use of S-Taliro for finding interesting property violations in a PID-based hybrid closed loop control system.

Diabetes cases worldwide have risen steadily over the past decades, lending urgency to the search for more efficient, effective, and personalized ways to treat the disease. Current treatment strategies, however, may fail to maintain ultradian oscillations in blood glucose concentration, an important element of a healthy alimentary system. Building upon recent successes in mathematical modeling of the human glucose-insulin system, we show that both food intake and insulin therapy likely demand increasingly precise control over insulin sensitivity if oscillations at a healthy average glucose concentration are to be maintained. We then suggest guidelines and personalized treatment options for diabetic patients that maintain these oscillations. We show that for a type II diabetic, both blood glucose levels can be controlled and healthy oscillations maintained when the patient gets an hour of daily exercise and is placed on a combination of Metformin and sulfonylurea drugs. We note that insulin therapy and an additional hour of exercise will reduce the patient’s need for sulfonylureas. Results of a modeling analysis suggest that a typical type I diabetic’s blood glucose levels can be properly controlled with a constant insulin infusion between 0.45 and 0.7 microU/(ml*min). Lastly, we note that all suggested strategies rely on existing clinical techniques and established treatment measures, and so could potentially be of immediate use in the design of an artificial pancreas.