Advances in technology give rise to increasingly robust and versatile home-use medical devices. Many of these devices are designed to monitor and interact with patients and their physiological systems to help maintain a particular level of health while permitting the patient to be mobile. Unfortunately, there is no well-established physics for human physiological systems and their coupling with medical devices. As a consequence, device designers have to resort to gathering empirical data in laboratory or other controlled environments to develop algorithms for approximating physiological systems. This can be expensive, incomplete, and fraught with inherent risks.

Unfortunately, there is no well-established physics for human physiological systems and their coupling with medical devices.

Academic research on hybrid automata shows the potential for precisely modeling both the computing aspects of home-use medical devices and their interaction with physiological systems using unified mathematical representations. Formal analysis and in-silico simulation can be performed on such representations. This makes possible a more comprehensive and complete assessment on the safety of these devices than traditional approaches.

In this paper, we examine the feasibility and advantages of applying hybrid automata to home-use medical devices, by constructing a non-linear hybrid automaton for a simple artificial pancreas (i.e., closed-loop insulin pump) model. This automaton formalizes the control logic of our artificial pancreas model as a finite state machine and specifies its interaction with the human glycemic system as differential equations. Our study shows that simulation using this automaton can expose potential design flaws in an artificial pancreas system.

Advances in technology have enabled the development of novel home-use medical devices to meet society's ever-growing demands for quality healthcare. Many of these devices are designed to work closely with patients by monitoring their physiological conditions to control and deliver appropriate therapy. This type of design, known as closedloop control, not only facilitates early detection of adverse medical conditions,1,2 but also enables autonomous decision making for appropriate therapy.

Designs of home-use devices, especially those with closed-loop control, should guarantee: 1) accurate and timely monitoring of patients' physiological condition(s), 2) correct prediction of the patients' needs for therapy, and 3) correct delivery of the predicted therapy. Many of these devices can be quite complex and present varying degrees of risk. It is important that such devices are safe and effective.

Assessing the safety of closed-loop home-use devices presents unique challenges. For example, it requires a profound understanding of the physics of human physiology, which is still being discovered. Moreover, the design of home-use devices must account for the patient's rapidly changing environments and varied physiological needs (e.g., change in energy needs from walking to running). Current assessment methods rely on experimentation and testing. This is not sufficient, because it only assesses the device under a limited set of scenarios and in controlled environments.

The theory of Hybrid Automata (HA)3 provides a mathematical means of describing both the continuous and discrete dynamics of complex (closed-loop) control systems, such as those found increasingly in home-use devices. Having such a mathematical representation provides a useful tool for assessing safety properties of these devices, because it allows characterizing these devices, including their functioning mechanisms, discrete control operations, and interaction with patients, into a unified (mathematical) framework.

The theory of Hybrid Automata (HA) provides a mathematical means of describing both the continuous and discrete dynamics of complex (closed-loop) control systems, such as those found increasingly in home-use devices.

This facilitates automatic analysis, including in-silico simulation, which can be performed on HA models to help manufacturers detect design flaws and other safety issues in their devices early in the design phase. More importantly, such analysis enables a more comprehensive assessment of these designs, as compared to current practices, by facilitating the exploration of a much broader set of behaviors from these designs.

In this paper, we demonstrate the usefulness of HA in home-use medical device design by applying it to a relatively simple, yet generic, artificial pancreas (AP), i.e., closed-loop insulin infusion pump, design. This study aims to assess the safety of the control strategy underlying this design. We construct a non-linear HA model that includes interaction with patients. Time-bounded simulations were performed on this model. Simulation results revealed that this design might cause hypo/hyperglycemia in diabetic patients.

AP devices4 are a good example of home-use devices with closed-loop control. Several novel AP (control) systems have been proposed and many are under clinical study. Most AP devices utilize one or more Continuous Glucose Monitor (CGM) sensors5 to constantly measure the patient's Blood Glucose (BG) level. This provides a basis for determining the amount of insulin (in the single hormone systems) or insulin and glucagon (in the bi-hormonal systems) to be delivered. Current AP devices use a variety of controllers, including proportional-integralderivative (PID) controllers,6 fuzzy logic controllers,7 and model predictive controllers.8 

In this paper, we consider a simple yet representative AP design (Figure 1)* comprising:

  • An insulin pump. This provides continuous (or near continuous) delivery of insulin.

    • – Insulin delivered throughout the day to meet the patient's variable background metabolic need is referred to as the basal insulin.

    • – Insulin delivered to address meals (carbohydrate intake) is referred to as the pre-prandial bolus insulin.

  • A CGM sensor. This continuously monitors the patient's interstitial glucose level and reports it to a remote receiver via wireless communication.

  • A remote computer-based controller. For example, the system receives interstitial glucose values from the CGM sensor, and the controller processes these values through a simple Kalman filter8 to predict the patient's blood glucose in the near future if the current insulin delivery rate remains unchanged. If the predicted level exceeds programmed bounds (lower and upper), the controller instructs the pump to adjust insulin delivery rate accordingly.

Figure 1.

Example of an Artificial Pancreas System

Figure 1.

Example of an Artificial Pancreas System

Close modal

More specifically, the controller uses a supervisory control algorithm to adjust insulin administration to keep the patient's BG level within a pre-specified safe range. The control algorithm decomposes the operation of the insulin pump into three discrete modes:

  1. Braking: This mode continuously adjusts the basal rate based on the level of risk implied by the projected BG level. The risk level, R(t), implied by a future BG level is calculated as follows: if the BG level after one hour, denoted as BG60min, >= 120 mg/dl, R(t) is set to 0; if BG60min <= 20 mg/dl, R(t) is set to 100; otherwise, R(t) is calculated as a non-linear logarithmic function of BG60min. The basal rate is then reduced by a fraction proportional to R(t).

  2. Meal Supervision: The system transitions into this mode if it is currently not in the Braking mode, and the patient is about to have a meal. Upon entering this mode, the control algorithm allows the patient to indicate the meal size (from three options), and then computes the dosage of insulin needed to compensate for the meal accordingly.

  3. Correction Bolus: The system transitions into this mode only when all of the following conditions hold: 1) it has been more than two hours since the last meal bolus, 2) it is not currently in the Braking mode, 3) at least one hour has passed since the last correction bolus, and 4) BG60min is predicted to be greater than 180 mg/dl. In this mode, a correction bolus is delivered to the patient, the size of which is calculated as a linear function of BG60min.

Hybrid Automata (HA). An HA consists of a finite set of discrete states and transitions among them, where each state contains a set of variables and each transition is labeled with a condition on the variables (of the source state). Each state of a HA is also defined with a set of differential equations to govern the values of variables in it. If all differential equations in a HA are linear, i.e., taking the form of equation 1, this automaton is linear.

formula

Given an HA A, each of its executions start from its initial state with a distinct initial condition, which defines the values of A's variables at the beginning of the execution. As the execution proceeds, the differential equations in A's current state are solved to update the values of all involved variables. These values are then used to evaluate the conditions labeled on transitions outgoing from A's current state. If any of such conditions are satisfied, the automaton takes the transition and enters into its destination state. Notably, entering into a new state can cause a new set of differential equations to be solved in the future, reflecting the changes in system dynamics.

Modeling Patient Insulin-Glucose Reaction. Formalizing the example AP design in Section 2 requires modeling the CGM sensor as well. However, if the focus is to evaluate the safety and correctness of the control strategy embedded in this design, then the engineering details of the CGM sensor can be replaced by a patient physiological model, such as the Bergman Minimal Model (BMM).10 

The BMM defines the interaction between insulin and the patient's blood glucose (either stored internally or provided through meals) as a set of non-linear ordinary differential equations, as illustrated in Equation 2, where G(t), X(t), and I(t) are the patient's BG level, and interstitial and plasma insulin concentration, respectively. In addition, in Equation 2, k1, k2, k3, k4, k5, k6, Ib, and Gb are patient-specific constants, derived either from empirical data or using diabetic patient simulators.10 

formula

The example AP design also needs input from the patient to indicate the timing and size of meal intakes. We adopt a zero mean Gaussian random process to model the patient's dietary behavior, where we assume the meal size, w(t), can only take values from the set {0,2.5,3,5}, as a way to abstract potential meal sizes for the sake of simplicity.

Constructing an HA Model for Artificial Pancreas. The HA model constructed for the example AP design contains three discrete states, each corresponding to one of the aforementioned operational modes. An additional state is introduced to represent basal infusion. Figure 2 depicts the structure of the model, in which each state shares a same set of variables, including X(t), G(t), and I(t). All these variables are governed by Equation 2.

Figure 2.

Artificial Pancreas Hybrid Automaton Model

Figure 2.

Artificial Pancreas Hybrid Automaton Model

Close modal

This automaton always starts execution from the Basal Infusion state, and then transits to other states based on corresponding transition conditions: It transits to the Braking state when BG60min is predicted to be less than 120 mg/dl, and returns back if it becomes greater; the transition to the Meal Supervision state is triggered if a meal is taken (w(t) > 0), and the automaton exits from this state after two hours (π > 120 mins); the automaton starts a correction bolus if BG60min is greater than 180mg/dl, and resumes the basal infusion one hour later.

In-silico HA models have been very useful in testing algorithms to ensure that they run appropriately and permit the investigator to test the range of parameters that the algorithm can handle. For example, simulating a HA model can reveal, to the extent permitted by simulation time and initial conditions, the presence of unsafe states. While in-silico models have allowed us to decrease the reliance on animal testing and allowed some decrease in developmental time, we have found that the algorithms generally have to be adjusted once testing with human subjects has begun. These models appear to be useful in the initial stages of system development but are not sufficient to test the range of dynamic changes and demands that are unique to each patient. Therefore, the current models would not obviate the need for well-designed clinical studies to evaluate the final system.

While in-silico models have allowed us to decrease the reliance on animal testing and allowed some decrease in developmental time, we have found that the algorithms generally have to be adjusted once testing with human subjects has begun.

We used the Breach package from the matrix laboratory (MATLAB) tool suite,11 to simulate the HA model presented in Section 3. Breach is a simulation and verification tool for analyzing dynamic systems with non-linear differential equations. Using Breach, we can establish desired safety boundaries and then see if the treatment boundary is exceeded. We used a generally acceptable lower boundary of 60 mg/dl§ and upper boundary of 250 mg/dl; recognizing that there are no hard thresholds that hold across all possible cases and that simulation of individual cases are likely warranted.

The time bound for the simulation was set as 10,000 seconds, and the initial states of the simulation were defined as {X(t), G(t), I(t)} = {[0, 0.1], [60, 180], [0, 100]}. Figure 3 illustrates the portion of state space explored during the simulation (shaded regions). As Figure 3 reveals, the model might lead diabetic patients into harmful situations such as hypoglycemia, because unsafe states (regions beyond the red threshold) were reached during the simulation.

Figure 3.

Simulation Results for AP-HA Model

Figure 3.

Simulation Results for AP-HA Model

Close modal

Simulation on HA models can expose the presence of device design errors if appropriate simulation time and initial conditions are selected. Developers will still need to establish the cause(s) of these errors and make appropriate corrections.

It is possible to analyze HA models more comprehensively using mathematical-based verification techniques, such as those described in Alur, 2011.12 We chose simulation to analyze the HA model because of the nonlinearity of the model. Complex systems such as human physiological systems typically demonstrate certain nonlinearities, i.e., the system output is not directly proportional to the input. Thus, the HA models constructed for these systems are nonlinear (see Equation 2 for instance). Mechanical reasoning of these models requires finding closed-form solutions for their nonlinear differential equations, which is often computationally expensive, and sometimes impossible.

This preliminary study applies the HA technique to a simple AP design. Many challenges, both technical and theoretical, have to be addressed when the HA technique is applied to real-world, complex devices. For example, to model realistic AP systems one has to consider noise factors and errors from CGM measurements, diffusion delay of insulin in subcutaneous tissues, and predictive models of human activities and physiology.

Failing to address these issues may result in significant discrepancies between a HA model and a real world system. The delta between model and real-world properties can be reduced but not eliminated through principled collaborations between designers and HA domain experts. Thus, system-level validation and clinical experimentation are still necessary to account for these facts.

A challenge limiting the applicability of HA models in closed-loop medical devices is the state space explosion phenomenon. For a complicated control system, its corresponding HA model can contain a large number of variables. Consequently, the state space of the model can be too large to handle. For example, the Kalman filter in Section 2 computes the predicted BG level as a linear function of previous BG values.

Modeling this predictor requires a large set of variables to store historic BG readings, because HA models are memory-less.13 One solution to this issue is to convert equations that imply a large state space into continuous differential equations. The tradeoff in this solution, however, is the potential discrepancy between the model and the “real world” system.

In this paper, we used a simple artificial pancreas design as an example to show that the hybrid-automata framework can be used to characterize and analyze the design of closedloop devices. This work is only a first step in our effort toward using hybrid automata to assess and improve the safety of (home-use) closed-loop medical devices. Future work might include a) applying hybrid automata techniques to more complex AP models or b) investigating additional verification techniques, such as reachability analysis for hybrid automata models, which may enable a more comprehensive assessment of home use device safety.

The work of Ayan Banerjee and Dr. Sandeep K.S. Gupta was funded in part by NSF grants CNS-0831544 and IIS-1116385.

1.
Stern
S
,
Tzivoni
D.
Early Detection of Silent Ischaemic Heart Disease by 24-hour Electrocardiographic Monitoring of Active subjects
.
Brit Heart J
.
1974
;
36
(
5
):
481
486
.
2.
Indiana University Health
.
Neuroscience Center
. .
3.
Girard
A
,
Pappas
GJ
,
Verification using simulation
,
Hybrid Sys: Comp and Control
.
2006
;
3927
:
272
286
.
4.
Bardin
J.
Trial of Artificial Pancreas Gives Diabetes Patients a Break
. .
5.
Castle
JR
,
Pitts
A
,
Hanvan
K
,
et al
.
The accuracy benefits of multiple amperometric glucose sensors in people with type 1 diabetes
.
Diabetes Care
.
2012
;
35
(
4
):
706
710
.
6.
Marchetti
G
,
Barolo
M
,
Jovanovic
L
,
Zisser
H
,
Seborg
DE
.
An Improved PID Switching Control Strategy for Type 1 Diabetes
.
IEEE Trans on Biomed Eng
.
2008
;
55
(
3
):
857
865
.
7.
Yasini
S
,
Naghibi-Sistani
MB
,
Karimpour
A
.
Active Insulin Infusion Using Fuzzy Based Closed Loop Control
.
Proc 3rd IEEE Int Conf on Intelligent System and Knowledge Engineering (ISKE)
.
2008
;
1
:
429
434
.
8.
Kovatchev
B
,
Patek
S
,
Dassau
E
,
et al
.
Control to Range for Diabetes: Functionality and Modular Architecture
.
J Diabetes Science and Tech
.
2009
;
3
(
5
):
1058
1065
.
9.
Patek
SD
,
Magni
L
,
Dassau
E
,
et al
.
Modular Closed-Loop Control of Diabetes
.
IEEE Trans on Biomed Eng
.
2012
;
59
(
11
):
2986
2999
.
10.
MLAB
.
MLAB Technical Application Notes: Bergman Minimal Model
.
Available at: www.civilized.com/mlabexamples/glucose.htmld/. Accessed Feb 10, 2013
.
11.
Donze
A.
Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems
.
Proc. 22nd Int Conf on Computer Aided Verification (CAV)
.
2010
;
7
:
167
170
.
12.
Alur
R.
Formal Verification of Hybrid Systems
.
Proc Int Conf on Embedded Software
.
2011
;
10
:
273
278
.
13.
TEG
.
T1DM: Type 1 Diabetes Metabolic Simulator
.
Available at: http://tegvirginia.com/solutions/t1dms/. Accessed on Feb. 10, 2013
.

* This model was first proposed by Kovatchev et al. in 2009.8 The sole reason for using the AP model in our study is to show the potential use of HA in home-used medical device design verification. For recent advances in AP technology, see for example Patek et al., 2012.9 

This is especially true for type-1 diabetic patients as potential users of AP devices. These patients usually demonstrate great diversity in internal glycemic systems, reaction to insulin, and personal behavior patterns, which require treatment plans unique to each patient.

§ 60 – 70 mg/dl is a common lower bound for an average patient. We used 60 mg/dl for our research.

About the Authors

Ayan Banerjee, PhD, is postdoctoral fellow at the IMPACT (Intelligent Mobile and Pervasive Applications and Computing Technologies) Lab, Arizona State University. E-mail: abanerj3@asu.edu

Yi Zhang, PhD, is visiting scientist in the Office of Science and Engineering Laboratory at the Center for Devices and Radiological Health, US Food and Drug Administration (FDA/CDRH). E-mail: yi.zhang2@fda.hhs.gov

Paul Jones, MS, is senior systems and software engineer in the Office of Science and Engineering Laboratories at the FDA/CDRH. E-mail: paul.jones@fda.hhs.gov

Sandeep K.S. Gupta, PhD, is professor of computer science and director of the IMPACT Lab, Arizona State University. E-mail: sandeep.gupta@asu.edu