Models, Devices, Properties, and Verification of Artificial Pancreas Systems

  • Taisa Kushner
  • B. Wayne Bequette
  • Faye Cameron
  • Gregory Forlenza
  • David Maahs
  • Sriram SankaranarayananEmail author
Part of the Computational Biology book series (COBO, volume 30)


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 the one hand, they hold the promise of easing the everyday burden of managing type 1 diabetes. On the other hand, 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.



The authors gratefully acknowledge detailed comments from the anonymous reviewers. This work was supported in part by the US National Science Foundation (NSF) under grant numbers 1446900, 1446751, and 1646556. All opinions expressed are those of the authors and not necessarily of the NSF.


  1. 1.
    Abbas H, Fainekos G, Sankaranarayanan S, Ivancic F, Gupta A (2013) Probabilistic temporal logic falsification of cyber-physical systems. Trans Embed Comput Syst (TECS) 12:95Google Scholar
  2. 2.
    Advisory R (2016) R7-2016-07: Multiple vulnerabilities in animas onetouch ping insulin pump. Cf.
  3. 3.
    Akaike H (1974) A new look at the statistical model identification. IEEE Trans Autom Control 19(6):716–723MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Alberti K, Zimmet P (1998) Definition, diagnosis and classification of diabetes mellitus and its complications. Part 1: diagnosis and classification of diabetes mellitus. Provisional report of a who consultation. Diabetic Med 15(7):539–553CrossRefGoogle Scholar
  5. 5.
    Alberts B, Johnson A, Lewis J, Raff M, Roberts K, Walter P (2002) Molecular biology of the cell, (garland science, New York, 2008). Google Scholar, p 652CrossRefGoogle Scholar
  6. 6.
    Annapureddy YSR, Liu C, Fainekos GE, Sankaranarayanan S (2011) S-taliro: A tool for temporal logic falsification for hybrid systems. In: Tools and algorithms for the construction and analysis of systems, vol 6605. LNCS. Springer, Berlin, pp 254–257Google Scholar
  7. 7.
    Atlas E, Nimri R, Miller S, Grunberg EA, Phillip M (2010) MD-Logic artificial pancreas system: A pilot study in adults with type 1 diabetes. Diabetes Care 33(5):1072–1076CrossRefGoogle Scholar
  8. 8.
    Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, CambridgezbMATHGoogle Scholar
  9. 9.
    Basu R, Di Camillo B, Toffolo G, Basu A, Shah P, Vella A, Rizza R, Cobelli C (2003) Use of a novel triple-tracer approach to assess postprandial glucose metabolism. Am J Physiol-Endocrinol Metab 284(1):E55–E69CrossRefGoogle Scholar
  10. 10.
    Baysal N, Cameron F, Buckingham BA, Wilson DM, Chase HP, Maahs DM, Bequette B (2014) A novel method to detect pressure-induced sensor attenuations (PISA) in an artificial pancreas. J Diabetes Sci Technol 8(6):1091–1096CrossRefGoogle Scholar
  11. 11.
    Bequette BW (2013) Algorithms for a closed-loop artificial pancreas: The case for model predictive control. J Diabetes Sci Technol 7:1632–1643CrossRefGoogle Scholar
  12. 12.
    Bequette B, Cameron F, Buckingham B, Maahs D, Lum J (2018) Overnight hypoglycemia and hyperglycemia mitigation for individuals with type 1 diabetes. How risks can be reduced. IEEE Control Syst 125–134.
  13. 13.
    Bergman RN (2005) Minimal model: Perspective from 2005. Hormone research, pp 8–15. Scholar
  14. 14.
    Bergman RN (2007) Orchestration of glucose homeostasis: From a small acorn to the california oak. Diabetes 56(6):1489–1501CrossRefGoogle Scholar
  15. 15.
    Bergman RN, Urquhart J (1971) The pilot gland approach to the study of insulin secretory dynamics. Recent Prog Horm Res 27:583–605Google Scholar
  16. 16.
    Bergman RN, Ider YZ, Bowden CR, Cobelli C (1979) Quantitative estimation of insulin sensitivity. Am J Physiol-Endocrinol Metab 236(6):E667CrossRefGoogle Scholar
  17. 17.
    Bertsimas D, Gupta V, Kallus N (2018) Data-driven robust optimization. Math. Program 167(2):235–292MathSciNetzbMATHCrossRefGoogle Scholar
  18. 18.
    Bolie VW (1961) Coefficients of normal blood glucose regulation. J Appl Physiol 16(5):783–788CrossRefGoogle Scholar
  19. 19.
    Borri A, Cacace F, De Gaetano A, Germani A, Manes C, Palumbo P, Panunzi S, Pepe P (2017) Luenberger-like observers for nonlinear time-delay systems with application to the artificial pancreas: The attainment of good performance. IEEE Control Syst 37(4):33–49MathSciNetCrossRefGoogle Scholar
  20. 20.
    Cameron F, Bequette BW, Wilson D, Buckingham B, Lee H, Niemeyer G (2011) Closed-loop artificial pancreas based on risk management. J Diabetes Sci Technol 5(2):368–379CrossRefGoogle Scholar
  21. 21.
    Cameron F, Niemeyer G, Bequette BW (2012) Extended multiple model prediction with application to blood glucose regulation. J Process Control 22(8):1422–1432CrossRefGoogle Scholar
  22. 22.
    Cameron F, Wilson DM, Buckingham BA, Arzumanyan H, Clinton P, Chase HP, Lum J, Maahs DM, Calhoun PM, Bequette BW (2012) Inpatient studies of a kalman-filter-based predictive pump shutoff algorithm. J Diabetes Sci Technol 6(5):1142–1147CrossRefGoogle Scholar
  23. 23.
    Cameron F, Niemeyer G, Wilson DM, Bequette BW, Benassi KS, Clinton P, Buckingham BA (2014) Inpatient trial of an artificial pancreas based on multiple model probabilistic predictive control with repeated large unannounced meals. Diabetes Technol Ther 728–734. Scholar
  24. 24.
    Cameron F, Fainekos G, Maahs DM, Sankaranarayanan S (2015) Towards a verified artificial pancreas: Challenges and solutions for runtime verification. In: Proceedings of runtime verification (RV 2015), vol 9333. Lecture notes in computer science, pp 3–17CrossRefGoogle Scholar
  25. 25.
    Cameron FM, Ly TT, Buckingham BA, Maahs DM, Forlenza GP, Levy CJ, Lam D, Clinton P, Messer LH, Westfall E, Levister C, Xie YY, Baysal N, Howsmon D, Patek SD, Bw B (2017) Closed-loop control without meal announcement in type 1 diabetes. Diabetes Technol Ther 19(9):527–532. Scholar
  26. 26.
    Chase HP, Maahs D (2011) Understanding diabetes (Pink Panther Book). Children’s diabetes foundation, 12 edn. Available online through CU Denver Barbara Davis Center for DiabetesGoogle Scholar
  27. 27.
    Chee F, Fernando T (2007) Closed-loop control of blood glucose. Springer, BerlinzbMATHGoogle Scholar
  28. 28.
    Chen X, Ábrahám E, Sankaranarayanan S (2013) Flow*: An analyzer for non-linear hybrid systems. In: Proceedings of CAV 2013, vol 8044. LNCS. Springer, Berlin, pp 258–263CrossRefGoogle Scholar
  29. 29.
    Chen S, O’Kelly M, Weimer J, Sokolsky O, Lee I (2015) An intraoperative glucose control benchmark for formal verification. In: 5th IFAC conference on analysis and design of hybrid systems (ADHS)Google Scholar
  30. 30.
    Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, CambridgeGoogle Scholar
  31. 31.
    Clarke WL, Anderson S, Breton M, Patek S, Kashmer L, Kovatchev B (2009) Closed-loop artificial pancreas using subcutaneous glucose sensing and insulin delivery and a model predictive control algorithm: The virginia experience. J Diabetes Sci Technol 3(5):1031–1038CrossRefGoogle Scholar
  32. 32.
    Cobelli C, Foster D, Toffolo G (2000) Tracer kinetics in biomedical research. Springer Science & Business Media, BerlinGoogle Scholar
  33. 33.
    Cobelli C, Man CD, Sparacino G, Magni L, Nicolao GD, Kovatchev BP (2009) Diabetes: Models, signals and control (methodological review). IEEE Rev Biomed Eng 2:54–95CrossRefGoogle Scholar
  34. 34.
    Cobelli C, Renard E, Kovatchev B (2011) Artificial pancreas: Past, present, future. Diabetes Care 60(11):2672–2682CrossRefGoogle Scholar
  35. 35.
    Cobelli C et al (2014) AP@Home Consortium. First use of model predictive control in outpatient wearable artificial pancreas. Diabetes Care 37(5):1212–1215CrossRefGoogle Scholar
  36. 36.
    Copp DA, Gondhalekar R, Hespanha JP (2018) Simultaneous model predictive control and moving horizon estimation for blood glucose regulation in type 1 diabetes. Optim Control Appl Methods 39(2):904–918MathSciNetzbMATHCrossRefGoogle Scholar
  37. 37.
    Cryer PE (2007) Hypoglycemia, functional brain failure, and brain death. J Clin Investig 117(4):868–870CrossRefGoogle Scholar
  38. 38.
    Cutler C, Ramaker B (1980) Dynamic matrix control a computer control algorithm. In: Proceedings of the joint automatic control conference. Paper WP5-BGoogle Scholar
  39. 39.
    de Moura LM, Bjørner N (2008) Z3: An efficient SMT solver. In: TACAS, vol 4963. LNCS. Springer, Berlin, pp 337–340Google Scholar
  40. 40.
    Diwakaran R, Sankaranarayanan S, Trivedi A (2017) Analyzing neighbourhoods of falsifying traces. In: International conference on CPS (to appear)Google Scholar
  41. 41.
    Dong Y, Hoover A, Scisco J, Muth E (2012) A new method for measuring meal intake in humans via automated wrist motion tracking. Appl Psychophysiol Biofeedback 37(3):205–215CrossRefGoogle Scholar
  42. 42.
    Donzé A (2010) Breach: A toolbox for verification and parameter synthesis of hybrid systems. In: CAV, vol 6174. Lecture notes in computer science. Springer, BerlinCrossRefGoogle Scholar
  43. 43.
    Donzé A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals. In: FORMATS, vol 6246. Lecture notes in computer science. Springer, Berlin, pp 92–106Google Scholar
  44. 44.
    Doyle FJ, Huyett LM, Lee JB, Zisser HC, Dassau E (2014) Closed-loop artificial pancreas systems: Engineering the algorithms. Diabetes Care 37:1191–1197CrossRefGoogle Scholar
  45. 45.
    Dunaif A, Finegood DT (1996) Beta-cell dysfunction independent of obesity and glucose intolerance in the polycystic ovary syndrome. J Clin Endocrinol Metab 81(3):942–947Google Scholar
  46. 46.
    Dutta S, Kushner T, Sankaranarayanan S (2018) Robust data-driven control of artificial pancreas systems using neural networks. In: International conference on computational methods in systems biology. Springer, Berlin, pp 183–202zbMATHCrossRefGoogle Scholar
  47. 47.
    El-Khatib FH, Russell SJ, Nathan DM, Sutherlin RG, Damiano ER (2010) A bihormonal closed-loop artificial panceras for type 1 diabetes. Sci Trans Med 2CrossRefGoogle Scholar
  48. 48.
    Facchinetti A, Sparacino G, Cobelli C (2010) Modeling the error of continuous glucose monitoring sensor data: Critical aspects discussed through simulation studies. J Diabetes Sci Technol 4(1)CrossRefGoogle Scholar
  49. 49.
    Fainekos G, Pappas GJ (2009) Robustness of temporal logic specifications for continuous-time signals. Theor Comput Sci 410:4262–4291MathSciNetzbMATHCrossRefGoogle Scholar
  50. 50.
    Forlenza G, Cameron F, Ly T, Lam D, Howsmon D, Baysal N, Kulina G, Messer L, Clinton P, Levister C, Patek S, Levy C, Wadwa R, Maahs D, Bequette B, Buckingham B (2018) Fully closed-loop multiple model predictive controller (mmppc) artificial pancreas (ap) performance in adolescents and adults in a supervised hotel setting. Diabetes Technol Ther 20:5. Scholar
  51. 51.
    Forlenza G, Deshpande S, Ly T, Howsmon D, Cameron F, Baysal N, Mauritzen E, Marcal T, Towers L, Bequette B, Huyett L, Pinsker J, Gondhalekar R, Doyle FI, Maahs D, Buckingham B, Dassau E (2017) Application of zone model predictive control artificial pancreas during extended use of infusion set and sensor: A randomized crossover-controlled home-use trial. Diabetes Care 40:1096–1102. Scholar
  52. 52.
    Fraley C, Raftery AE (1998) How many clusters? which clustering method? answers via model-based cluster analysis. Comput J 41(8):578–588zbMATHCrossRefGoogle Scholar
  53. 53.
    Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: Scalable verification of hybrid systems. In: Proceedings of CAV 2011, vol 6806. LNCS, pp 379–395CrossRefGoogle Scholar
  54. 54.
    Gao S, Kong S, Clarke EM (2013) dReal: An SMT solver for nonlinear theories over the reals. In: Proceedings of CADE 2013, vol 7898. Lecture notes in computer science. Springer, Berlin, pp 208–214Google Scholar
  55. 55.
    Garcia G, Morshedi A (1986) Quadratic programming solution of dynamic matrix control (QDMC). Chem Eng Commun 46:73–87CrossRefGoogle Scholar
  56. 56.
    Garg SK, Weinzimer SA, Tamborlane WV, Buckingham BA, others (2017) Glucose outcomes with the in-home use of a hybrid closed-loop insulin delivery system in adolescents and adults with type 1 diabetes. Diabetes Technol Ther 19(3):1–9CrossRefGoogle Scholar
  57. 57.
    Georga EI, Protopappas VC, Polyzos D, Fotiadis DI (2012) A predictive model of subcutaneous glucose concentration in type 1 diabetes based on random forests. In: 2012 annual international conference of the IEEE engineering in medicine and biology society (EMBC). IEEE, pp 2889–2892Google Scholar
  58. 58.
    Georga EI, Protopappas VC, Ardigò D, Marina M, Zavaroni I, Polyzos D, Fotiadis DI (2013) Multivariate prediction of subcutaneous glucose concentration in type 1 diabetes patients based on support vector regression. IEEE J Biomed Health Inform 17(1):71–81CrossRefGoogle Scholar
  59. 59.
    Ghorbani M, Bogdan P (2014) Reducing risk of closed loop control of blood glucose in artificial pancreas using fractional calculus. In: 36th annual international conference of the IEEE engineering in medicine and biology society (EMBS), pp 4839–4842Google Scholar
  60. 60.
    Gondhalekar R, Dassau E, Doyle FJ (2014) Moving-horizon-like state estimation via continuous glucose monitor feedback in mpc of an artificial pancreas for type 1 diabetes. In: 2014 IEEE 53rd annual conference on decision and control (CDC). IEEE, pp 310–315Google Scholar
  61. 61.
    Gondhalekar R, Dassau E, Doyle FJ III (2016) Periodic zone-mpc with asymmetric costs for outpatient-ready safety of an artificial pancreas to treat type 1 diabetes. Automatica 71:237–246MathSciNetzbMATHCrossRefGoogle Scholar
  62. 62.
    Griva L, Breton M, Chernavvsky D, Basualdo M (2017) Commissioning procedure for predictive control based on arx models of type 1 diabetes mellitus patients. IFAC-PapersOnLine 50(1):11023–11028CrossRefGoogle Scholar
  63. 63.
    Grosman B, Dassau E, Zisser H, Jovanovic L, Doyle F (2010a) Zone model predictive control: A strategy to minimize hyper- and hypoglycemic events. J Diabetes Sci Technol 4(4):961–975CrossRefGoogle Scholar
  64. 64.
    Grosman B, Dassau E, Zisser HC, Jovanovič L, Doyle FJ (2010b) Zone model predictive control: A strategy to minimize hyper- and hypoglycemic events. J Diabetes Sci Technol 4(4):961–975CrossRefGoogle Scholar
  65. 65.
    Grosman B, Wu D, Miller D, Lintereur L, Roy A, Parikh N, Kaufman FR (2018) Sensor-augmented pump-based customized mathematical model for type 1 diabetes. Diabetes Technol Ther 20(3):207–221CrossRefGoogle Scholar
  66. 66.
    Hakami H (Medtronic Inc.). FDA approves MINIMED 670G system - world’s first hybrid closed loop system.
  67. 67.
    Hamby DM (1994) A review of techniques for parameter sensitivity analysis of environmental models. Environ Monit Assess 32(2):135–154CrossRefGoogle Scholar
  68. 68.
    HAPIfork. HAPIfork. Accessed 26 Feb 2017
  69. 69.
    Harvey R, Dassau E et al (2014) Clinical evaluation of an automated artificial pancreas using zone-model predictive control and health monitoring system. Diabetes Technol Ther 16:348–357CrossRefGoogle Scholar
  70. 70.
    Hovorka R (2005) Continuous glucose monitoring and closed-loop systems. Diabetic Med 23(1):1–12CrossRefGoogle Scholar
  71. 71.
    Hovorka R, Shojaee-Moradie F, Carroll P, Chassin L, Gowrie I, Jackson N, Tudor R, Umpleby A, Hones R (2002) Partitioning glucose distribution/transport, disposal and endogenous production during IVGTT. Am J Physiol Endocrinol Metab 282:992–1007CrossRefGoogle Scholar
  72. 72.
    Hovorka R, Canonico V, Chassin L, Haueter U, Massi-Benedetti M, Frederici M, Pieber T, Shaller H, Schaupp L, Vering T, Wilinska M (2004) Nonlinear model predictive control of glucose concentration in subjects with type 1 diabetes. Physiol Meas 25:905–920CrossRefGoogle Scholar
  73. 73.
    Howsmon DP, Baysal N, Buckingham BA, Forlenza GP, Ly TT, Maahs DM, Marcal T, Towers L, Mauritzen E, Deshpande S, Huyett LM, Pinsker JE, Gondhalekar R III, FJD, Dassau E, Hahn J, Bequette BW (2018) Real-time detection of infusion site failures in a closed-loop artificial pancreas. Diabetes Sci Technol.
  74. 74.
    Howsmon DP, Cameron F, Baysal N, Ly TT, Forlenza GP, Maahs DM, Buckingham BA, Hahn J, Bequette BW (2017) Continuous glucose monitoring enables the detection of losses in infusion set actuation (LISAs). Sensors 17. Scholar
  75. 75.
    Iii FJD, Huyett LM, Lee JB, Zisser HC, Dassau E (2014) Closed-loop artificial pancreas systems: Engineering the algorithms. Diabetes Care 37(5):1191–1197CrossRefGoogle Scholar
  76. 76.
    Jacobs PG, Resalat N, El Youssef J, Reddy R, Branigan D, Preiser N, Condon J, Castle J (2015) Incorporating an exercise detection, grading, and hormone dosing algorithm into the artificial pancreas using accelerometry and heart rate. J Diabetes Sci Technol 9(6):1175–1184CrossRefGoogle Scholar
  77. 77.
    Jayalakshmi T, Santhakumaran A (2010) A novel classification method for diagnosis of diabetes mellitus using artificial neural networks. In: 2010 international conference on data storage and data engineering (DSDE). IEEE, pp 159–163Google Scholar
  78. 78.
    Kissler SM, Cichowitz C, Sankaranarayanan S, Bortz DM (2014) Determination of personalized diabetes treatment plans using a two-delay model. J Theor Biol (accepted)Google Scholar
  79. 79.
    Korytkowski MT, Berga SL, Horwitz MJ (1995) Comparison of the minimal model and the hyperglycemic clamp for measuring insulin sensitivity and acute insulin response to glucose. Metabolism 44(9):1121–1125CrossRefGoogle Scholar
  80. 80.
    Kovatchev BP, Breton M, Man CD, Cobelli C (2009) In silico preclinical trials: a proof of concept in closed-loop control of type 1 diabetesGoogle Scholar
  81. 81.
    Kowalski A (2015) Pathway to artificial pancreas revisited: Moving downstream. Diabetes Care 38:1036–1043CrossRefGoogle Scholar
  82. 82.
    Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255–299CrossRefGoogle Scholar
  83. 83.
    Kushner T, Bortz D, Maahs D, Sankaranarayanan S (2018) A data-driven approach to artificial pancreas verification and synthesis. In: International conference on cyber-physical systems (ICCPS 2018). IEEE PressGoogle Scholar
  84. 84.
    Kusunoki J, Kanatani A, Moller DE (2006) Modulation of fatty acid metabolism as a potential approach to the treatment of obesity and the metabolic syndrome. Endocrine 29(1):91–100CrossRefGoogle Scholar
  85. 85.
    Lee H, Bequette B (2009) A closed-loop artificial pancreas based on MPC: Human-friendly identification and automatic meal disturbance rejection. Biomed Signal Process Control 4(4):347–354CrossRefGoogle Scholar
  86. 86.
    Lee H, Buckingham B, Wilson D, Bequette B (2009) A closed-loop artificial pancreas using model predictive control and a sliding meal size estimator. J Diabetes Sci Technol 3(5):1082–1090CrossRefGoogle Scholar
  87. 87.
    Lehmann E, Deutsch T (1992) A physiological model of glucose-insulin interaction in type 1 diabetes mellitus. J Biomed Eng 14(3):235–242CrossRefGoogle Scholar
  88. 88.
    Li J, Kuang Y, Li B (2001) Analysis of ivgtt glucose-insulin interaction models with time delay. Discret Contin Dyn Syst Ser B 1(1):103–124MathSciNetzbMATHCrossRefGoogle Scholar
  89. 89.
    Li J, Kuang Y, Mason CC (2006) Modeling the glucose-insulin regulatory system and ultradian insulin secretory oscillations with two explicit time delays. J Theor Biol 242(3):722–735MathSciNetCrossRefGoogle Scholar
  90. 90.
    Li C, Raghunathan A, Jha NK (2011) Hijacking an insulin pump: Security attacks and defenses for a diabetes therapy system. In: International Conference on e-health networking, applications and security, pp 151–156Google Scholar
  91. 91.
    Liepe J, Kirk P, Filippi S, Toni T, Barnes CP, Stumpf MPH (2014) A framework for parameter estimation and model selection from experimental data in systems biology using approximate bayesian computation. Nat Protoc 9(2):439–456CrossRefGoogle Scholar
  92. 92.
    Liu J, Johns E, Atallah L, Pettitt C, Lo B, Frost G, Yang GZ (2012) An intelligent food-intake monitoring system using wearable sensors. In: 2012 ninth international conference on wearable and implantable body sensor networks, pp 154–160Google Scholar
  93. 93.
    Lunze K, Singh T, Walter M, Brendel MD, Leonhardt S (2013) Blood glucose control algorithms for type 1 diabetic patients: A methodological review. Biomed Signal Process Control 8(2):107 – 119. ISSN 1746–8094CrossRefGoogle Scholar
  94. 94.
    Maahs DM, Calhoun P, Buckingham BA, Others (2014) A randomized trial of a home system to reduce nocturnal hypoglycemia in type 1 diabetes. Diabetes Care 37(7):1885–1891CrossRefGoogle Scholar
  95. 95.
    Mahmoudi Z, Cameron F, Poulsen NK, Madsen H, Bequette BW, Jørgensen JB (2019) Sensor-based detection and estimation of meal carbohydrates for people with diabetes. Biomed Signal Process Control 48:12–25CrossRefGoogle Scholar
  96. 96.
    Makroglou A, Li J, Kuang Y (2006) Mathematical models and software tools for the glucose-insulin regulatory system and diabetes: An overview. Appl Numer Math 56(3–4):559–573MathSciNetzbMATHCrossRefGoogle Scholar
  97. 97.
    Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Formal techniques, modelling and analysis of timed and fault-tolerant systems. Springer, Berlin, pp 152–166zbMATHCrossRefGoogle Scholar
  98. 98.
    Man CD, Breton MD, Cobelli C (2009) Physical activity into the meal glucose-insulin model of type 1 diabetes: in silico studiesGoogle Scholar
  99. 99.
    Man CD, Camilleri M, Cobelli C (2006) A system model of oral glucose absorption: validation on gold standard data. IEEE Trans Biomed Eng 53(12):2472–2478CrossRefGoogle Scholar
  100. 100.
    Man C, Camilleri M, Cobelli C (2006) A system model of oral glucose absorption: Validation on gold standard data. IEEE Trans Biomed Eng 53(12):2472–2478CrossRefGoogle Scholar
  101. 101.
    Man CD, Micheletto F, Lv D, Breton M, Kovatchev B, Cobelli C (2014) The uva/padova type 1 diabetes simulator: New features. J Diabetes Sci Technol 8(1):26–34CrossRefGoogle Scholar
  102. 102.
    Man CD, Rizza RA, Cobelli C (2006) Meal simulation model of the glucose-insulin system. IEEE Trans Biomed Eng 1(10):1740–1749Google Scholar
  103. 103.
    Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, New YorkzbMATHCrossRefGoogle Scholar
  104. 104.
    Marchetti G, Barolo M, Jovanovič L, Zisser H, Seborg DE (2008) A feedforward-feedback glucose control strategy for type 1 diabetes mellitus. J Process Control 18(2):149–162CrossRefGoogle Scholar
  105. 105.
    Marieb E, Hoehn K (2004) Human anatomy and physiology 2004. Daryl Fox, San FranciscoGoogle Scholar
  106. 106.
    Mauseth R, Wang Y, Dassau E, Kircher R, Matheson D, Zisser H, others (2010) Proposed clinical application for tuning fuzzy logic controller of artificial pancreas utilizing a personalization factor. J Diabetes Sci Technol 4:913–922CrossRefGoogle Scholar
  107. 107.
    Musi N, Goodyear LJ (2006) Insulin resistance and improvements in signal transduction. Endocrine 29(1):73–80CrossRefGoogle Scholar
  108. 108.
    Muske KR, Badgwell TA (2002) Disturbance modeling for offset-free linear model predictive control. J Process Control 12:617–632CrossRefGoogle Scholar
  109. 109.
    Nghiem T, Sankaranarayanan S, Fainekos GE, Ivančić F, Gupta A, Pappas GJ (2010) Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Hybrid systems: computation and control. ACM Press, pp 211–220Google Scholar
  110. 110.
    Nguyen A, Alqurashi R, Raghebi Z, Banaei-kashani F, Halbower AC, Vu T (2016) A lightweight and inexpensive in-ear sensing system for automatic whole-night sleep stage monitoring. In: Proceedings of the 14th ACM conference on embedded network sensor systems CD-ROM, SenSys 2016, pp 230–244Google Scholar
  111. 111.
    Nicolao GD, Magni L, Man CD, Cobelli C (2011) Modeling and control of diabetes: Towards the artificial pancreas. IFAC Proc Vol 44(1):7092 – 7101. 18th IFAC World CongressGoogle Scholar
  112. 112.
    Nimri R, Muller I, Atlas E, Miller S, Kordonouri O, Bratina N, Tsioli C, Stefanija M, Danne T, Battelino T, Phillip M (2014) Night glucose control with md-logic artificial pancreas in home setting: a single blind, randomized crossover trial-interim analysis. Pediatr Diabetes 15(2):91–100CrossRefGoogle Scholar
  113. 113.
    Nucci G, Cobelli C (2000) Models of subcutaneous insulin kinetics. A critical review. Comput Methods Programs Biomed 62(3):249–257CrossRefGoogle Scholar
  114. 114.
    Otis B, Parviz B (2014) Introducing google’s smart contact lens project. Blog post on Google Inc. official weblog,
  115. 115.
    Paoletti N, Liu KS, Smolka SA, Lin S (2017) Data-driven robust control for type 1 diabetes under meal and exercise uncertainties. In: Computational methods in systems biology (CMSB), vol 10545. Lecture notes in computer science. Springer, Berlin, pp 214–232CrossRefGoogle Scholar
  116. 116.
    Parker RS, Doyle FJ III, Ward JH, Peppas NA (2000) Robust h glucose control in diabetes using a physiological model. AIChE J 46(12):2537–2549CrossRefGoogle Scholar
  117. 117.
    Parker RS, Doyle FJ, Peppas NA (2001) The intravenous route to blood glucose control. IEEE Eng Med Biol Mag 20(1):65–73CrossRefGoogle Scholar
  118. 118.
    Patek S, Bequette B, Breton M, Buckingham B, Dassau E, Doyle F III, Lum J, Magni L, Zisser H (2009) In silico preclinical trials: methodology and engineering guide to closed-loop control in type 1 diabetes mellitus. J Diabetes Sci Technol 3(2):269–282CrossRefGoogle Scholar
  119. 119.
    Pérez-Gandía C, Facchinetti A, Sparacino G, Cobelli C, Gómez E, Rigla M, de Leiva A, Hernando M (2010) Artificial neural network algorithm for online glucose prediction from continuous glucose monitoring. Diabetes Technol Ther 12(1):81–88CrossRefGoogle Scholar
  120. 120.
    Pillonetto G, Sparacino G, Cobelli C (2003) Numerical non-identifiability regions of the minimal model of glucose kinetics: superiority of bayesian estimation. Math Biosci 184(1):53–67MathSciNetzbMATHCrossRefGoogle Scholar
  121. 121.
    Pinsker JE, Lee JB, Dassau E, Seborg DE, Bradley PK, Gondhalekar R, Bevier WC, Huyett L, Zisser HC, Doyle FJ (2016) Randomized crossover comparison of personalized mpc and pid control algorithms for the artificial pancreas. Diabetes Care 39(7):1135–1142CrossRefGoogle Scholar
  122. 122.
    Platzer A (2008) Differential dynamic logic for hybrid systems. J Autom Reason 41(2):143–189MathSciNetzbMATHCrossRefGoogle Scholar
  123. 123.
    Plis K, Bunescu RC, Marling C, Shubrook J, Schwartz F (2014) A machine learning approach to predicting blood glucose levels for diabetes management. AAAI Work: Mod Artif Intell Health Anal 31:35–39Google Scholar
  124. 124.
    Polonsky KS, Sturis J, Van Cauter E (1998) Temporal profiles and clinical significance of pulsatile insulin secretion. Horm Res Paediatr 49(3–4):178–184CrossRefGoogle Scholar
  125. 125.
    Radcliffe J (2011) Hacking medical devices for fun and insulin: Breaking the human SCADA system. Black Hat 2011, Cf.
  126. 126.
    Ramkissoon C, Aufderheide B, Bequette BW, Vehi J (2017) Safety and hazards associated with the artificial pancreas. IEEE Rev Biomed Eng 10:44–52CrossRefGoogle Scholar
  127. 127.
    Rawlings J, Mayne D, Diehl M (2017) Model predictive control: theory, computation and design. Nob Hill Publishing, MadisonGoogle Scholar
  128. 128.
    Resalat N, El Youssef J, Reddy R, Jacobs PG (2016) Design of a dual-hormone model predictive control for artificial pancreas with exercise model. In: 2016 IEEE 38th annual international conference of the engineering in medicine and biology society (EMBC). IEEE, pp 2270–2273Google Scholar
  129. 129.
    Ruiz JL, Sherr JL, Cengiz E, Carria L, Roy A, Voskanyan G, Tamborlane WV, Weinzimer SA (2012) Effect of insulin feedback on closed-loop glucose control: A crossover study. J Diabetes Sci Technol 6(5):1123–1130CrossRefGoogle Scholar
  130. 130.
    Saad MF, Rebrin K, Steil GM et al (2006) Modeling glucose profiles obtained using closed loop insulin delivery-implications for controller optimization. Diabetes 55:A98CrossRefGoogle Scholar
  131. 131.
    Sankaranarayanan S, Kumar SA, Cameron F, Bequette BW, Fainekos G, Maahs DM (2017) Model-based falsification of an artificial pancreas control system. ACM SIGBED Review (Special Issue on Medical Cyber Physical Systems)Google Scholar
  132. 132.
    Shmarov F, Paoletti N, Bartocci E, Lin S, Smolka S, Zuliani P (2017) SMT-based synthesis of safe and robust PID controllers for stochastic hybrid systems. In: Hardware and software: verification and testing - 13th international haifa verification conference. Springer, Berlin, pp 131–146., Scholar
  133. 133.
    Siper MJ (2005) An introduction to mathematical theory of computation, 2nd edn. Thompson Publishing (Course Technology)Google Scholar
  134. 134.
    Skyler JS (ed) (2012) Atlas of Diabetes, 4th edn. Springer Science + Business MediaGoogle Scholar
  135. 135.
    Spaic T, Driscoll M, Raghiaru D, Buckingham B, Wilson D, Clinton P, Chase HP, Maahs D, Forlenza G, Jost E, Hramiak I, Paul T, Bequette B, Cameron F, Beck R, Kollan C, Lum J, Ly T (2017) Predictive hyperglycemia and hypoglycemia minimization: In-home evaluation of safety, feasibility, and efficacy in overnight control in type 1 diabetes. Diabetes Care 40(3):359–366. Scholar
  136. 136.
    Srinivasan R, Kadish AH, Sridhar R (1970) A mathematical model for the control mechanism of free fatty acid-glucose metabolism in normal humans. Comput Biomed Res 3(2):146–165CrossRefGoogle Scholar
  137. 137.
    Steil GM (2013) Algorithms for a closed-loop artificial pancreas: The case for proportional-integral-derivative control. J Diabetes Sci Technol 7:1621–1631CrossRefGoogle Scholar
  138. 138.
    Steil G, Panteleon A, Rebrin K (2004) Closed-sloop insulin delivery - the path to physiological glucose control. Adv Drug Deliv Rev 56(2):125–144CrossRefGoogle Scholar
  139. 139.
    Turksoy K, Cinar A (2018) Multi-module multivariable artificial pancreas for patients with type 1 diabetes. IEEE Control Syst Mag 38(1):105–124CrossRefGoogle Scholar
  140. 140.
    Turksoy K, Bayrak ES, Quinn L, Littlejohn E, Cinar A (2013) Multivariable adaptive closed-loop control of an artificial pancreas without meal and activity announcement. J Diabetes Technol Ther 15(5):386–400CrossRefGoogle Scholar
  141. 141.
    Turksoy K, Hajizadeh I, Samadi S, Feng J, Sevil M, Park M, Quinn L, Littlejohn E, Cinar A (2017) Real-time insulin bolusing for unannounced meals with artificial pancreas. Control Eng Practice 59:159–164. Scholar
  142. 142.
    Walsh J, Roberts R, Bailey T (2010) Guidelines for insulin dosing in continuous subcutaneous insulin infusion using new formulas from a retrospective study of individuals with optimal glucose levels. J Diabetes Sci Technol 4:1174–1181CrossRefGoogle Scholar
  143. 143.
    Weinzimer S, Steil G, Swan K, Dziura J, Kurtz N, Tamborlane W (2008) Fully automated closed-loop insulin delivery versus semiautomated hybrid control in pediatric patients with type 1 diabetes using an artificial pancreas. Diabetes Care 31:934–939CrossRefGoogle Scholar
  144. 144.
    Wilinska M, Chassin L, Acerini CL, Allen JM, Dunber D, Hovorka R (2010) Simulation environment to evaluate closed-loop insulin delivery systems in type 1 diabetes. J Diabetes Sci Technol 4CrossRefGoogle Scholar
  145. 145.
    Zavitsanou S, Chakrabarty A, Dassau E, Doyle FJ (2016) Embedded control in wearable medical devices: Application to the artificial pancreas. Processes 4(4)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Taisa Kushner
    • 1
  • B. Wayne Bequette
    • 2
  • Faye Cameron
    • 2
  • Gregory Forlenza
    • 3
  • David Maahs
    • 4
  • Sriram Sankaranarayanan
    • 1
    Email author
  1. 1.University of ColoradoBoulderUSA
  2. 2.Rensselaer Polytechnic InstituteTroyUSA
  3. 3.Barbara Davis Center for DiabetesUniversity of Colorado Anschutz Medical CampusDenverUSA
  4. 4.Stanford University Medical CenterStanfordUSA

Personalised recommendations