Skip to main content
SpringerLink
Log in

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

  • Chapter
  • First Online:
Automated Reasoning for Systems Biology and Medicine

Part of the book series: Computational Biology ((COBO,volume 30))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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:95

    Google Scholar 

  2. Advisory R (2016) R7-2016-07: Multiple vulnerabilities in animas onetouch ping insulin pump. Cf. https://community.rapid7.com/community/infosec/blog/2016/10/04/r7-2016-07-multiple-vulnerabilities-in-animas-onetouch-ping-insulin-pump

  3. Akaike H (1974) A new look at the statistical model identification. IEEE Trans Autom Control 19(6):716–723

    Article  MathSciNet  MATH  Google Scholar 

  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–553

    Article  Google Scholar 

  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 652

    Book  Google Scholar 

  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–257

    Google Scholar 

  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–1076

    Article  Google Scholar 

  8. Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge

    MATH  Google Scholar 

  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–E69

    Article  Google Scholar 

  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–1096

    Article  Google Scholar 

  11. Bequette BW (2013) Algorithms for a closed-loop artificial pancreas: The case for model predictive control. J Diabetes Sci Technol 7:1632–1643

    Article  Google Scholar 

  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. https://doi.org/10.1109/MCS.2017.2767119

  13. Bergman RN (2005) Minimal model: Perspective from 2005. Hormone research, pp 8–15. https://doi.org/10.1159/000089312

    Article  Google Scholar 

  14. Bergman RN (2007) Orchestration of glucose homeostasis: From a small acorn to the california oak. Diabetes 56(6):1489–1501

    Article  Google Scholar 

  15. Bergman RN, Urquhart J (1971) The pilot gland approach to the study of insulin secretory dynamics. Recent Prog Horm Res 27:583–605

    Google Scholar 

  16. Bergman RN, Ider YZ, Bowden CR, Cobelli C (1979) Quantitative estimation of insulin sensitivity. Am J Physiol-Endocrinol Metab 236(6):E667

    Article  Google Scholar 

  17. Bertsimas D, Gupta V, Kallus N (2018) Data-driven robust optimization. Math. Program 167(2):235–292

    Article  MathSciNet  MATH  Google Scholar 

  18. Bolie VW (1961) Coefficients of normal blood glucose regulation. J Appl Physiol 16(5):783–788

    Article  Google Scholar 

  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–49

    Article  MathSciNet  Google Scholar 

  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–379

    Article  Google Scholar 

  21. Cameron F, Niemeyer G, Bequette BW (2012) Extended multiple model prediction with application to blood glucose regulation. J Process Control 22(8):1422–1432

    Article  Google Scholar 

  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–1147

    Article  Google Scholar 

  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. https://doi.org/10.1089/dia.2014.0093

    Article  Google Scholar 

  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–17

    Chapter  Google Scholar 

  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. https://doi.org/10.1089/dia.2017.0078

    Article  Google Scholar 

  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 Diabetes

    Google Scholar 

  27. Chee F, Fernando T (2007) Closed-loop control of blood glucose. Springer, Berlin

    MATH  Google Scholar 

  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–263

    Chapter  Google Scholar 

  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. Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge

    Google Scholar 

  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–1038

    Article  Google Scholar 

  32. Cobelli C, Foster D, Toffolo G (2000) Tracer kinetics in biomedical research. Springer Science & Business Media, Berlin

    Google Scholar 

  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–95

    Article  Google Scholar 

  34. Cobelli C, Renard E, Kovatchev B (2011) Artificial pancreas: Past, present, future. Diabetes Care 60(11):2672–2682

    Article  Google Scholar 

  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–1215

    Article  Google Scholar 

  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–918

    Article  MathSciNet  MATH  Google Scholar 

  37. Cryer PE (2007) Hypoglycemia, functional brain failure, and brain death. J Clin Investig 117(4):868–870

    Article  Google Scholar 

  38. Cutler C, Ramaker B (1980) Dynamic matrix control a computer control algorithm. In: Proceedings of the joint automatic control conference. Paper WP5-B

    Google Scholar 

  39. de Moura LM, Bjørner N (2008) Z3: An efficient SMT solver. In: TACAS, vol 4963. LNCS. Springer, Berlin, pp 337–340

    Google Scholar 

  40. Diwakaran R, Sankaranarayanan S, Trivedi A (2017) Analyzing neighbourhoods of falsifying traces. In: International conference on CPS (to appear)

    Google Scholar 

  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–215

    Article  Google Scholar 

  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, Berlin

    Chapter  Google Scholar 

  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–106

    Google Scholar 

  44. Doyle FJ, Huyett LM, Lee JB, Zisser HC, Dassau E (2014) Closed-loop artificial pancreas systems: Engineering the algorithms. Diabetes Care 37:1191–1197

    Article  Google Scholar 

  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–947

    Google Scholar 

  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–202

    Chapter  MATH  Google Scholar 

  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 2

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  49. Fainekos G, Pappas GJ (2009) Robustness of temporal logic specifications for continuous-time signals. Theor Comput Sci 410:4262–4291

    Article  MathSciNet  MATH  Google Scholar 

  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. https://doi.org/10.1089/dia.2017.0424

    Article  Google Scholar 

  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. https://doi.org/10.2337/dc17-0500

    Article  Google Scholar 

  52. Fraley C, Raftery AE (1998) How many clusters? which clustering method? answers via model-based cluster analysis. Comput J 41(8):578–588

    Article  MATH  Google Scholar 

  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–395

    Chapter  Google Scholar 

  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–214

    Google Scholar 

  55. Garcia G, Morshedi A (1986) Quadratic programming solution of dynamic matrix control (QDMC). Chem Eng Commun 46:73–87

    Article  Google Scholar 

  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–9

    Article  Google Scholar 

  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–2892

    Google Scholar 

  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–81

    Article  Google Scholar 

  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–4842

    Google Scholar 

  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–315

    Google Scholar 

  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–246

    Article  MathSciNet  MATH  Google Scholar 

  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–11028

    Article  Google Scholar 

  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–975

    Article  Google Scholar 

  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–975

    Article  Google Scholar 

  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–221

    Article  Google Scholar 

  66. Hakami H (Medtronic Inc.). FDA approves MINIMED 670G system - world’s first hybrid closed loop system. https://www.medtronicdiabetes.com/blog/fda-approves-minimed-670g-system-worlds-first-hybrid-closed-loop-system/

  67. Hamby DM (1994) A review of techniques for parameter sensitivity analysis of environmental models. Environ Monit Assess 32(2):135–154

    Article  Google Scholar 

  68. HAPIfork. HAPIfork. https://www.hapi.com/product/hapifork. Accessed 26 Feb 2017

  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–357

    Article  Google Scholar 

  70. Hovorka R (2005) Continuous glucose monitoring and closed-loop systems. Diabetic Med 23(1):1–12

    Article  Google Scholar 

  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–1007

    Article  Google Scholar 

  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–920

    Article  Google Scholar 

  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. https://doi.org/10.1177/19322968187551.Online

  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. https://doi.org/10.3390/s17010161

    Article  Google Scholar 

  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–1197

    Article  Google Scholar 

  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–1184

    Article  Google Scholar 

  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–163

    Google Scholar 

  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. 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–1125

    Article  Google Scholar 

  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 diabetes

    Google Scholar 

  81. Kowalski A (2015) Pathway to artificial pancreas revisited: Moving downstream. Diabetes Care 38:1036–1043

    Article  Google Scholar 

  82. Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255–299

    Article  Google Scholar 

  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 Press

    Google Scholar 

  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–100

    Article  Google Scholar 

  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–354

    Article  Google Scholar 

  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–1090

    Article  Google Scholar 

  87. Lehmann E, Deutsch T (1992) A physiological model of glucose-insulin interaction in type 1 diabetes mellitus. J Biomed Eng 14(3):235–242

    Article  Google Scholar 

  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–124

    Article  MathSciNet  MATH  Google Scholar 

  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–735

    Article  MathSciNet  Google Scholar 

  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–156

    Google Scholar 

  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–456

    Article  Google Scholar 

  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–160

    Google Scholar 

  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–8094

    Article  Google Scholar 

  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–1891

    Article  Google Scholar 

  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–25

    Article  Google Scholar 

  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–573

    Article  MathSciNet  MATH  Google Scholar 

  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–166

    Chapter  MATH  Google Scholar 

  98. Man CD, Breton MD, Cobelli C (2009) Physical activity into the meal glucose-insulin model of type 1 diabetes: in silico studies

    Google Scholar 

  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–2478

    Article  Google Scholar 

  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–2478

    Article  Google Scholar 

  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–34

    Article  Google Scholar 

  102. Man CD, Rizza RA, Cobelli C (2006) Meal simulation model of the glucose-insulin system. IEEE Trans Biomed Eng 1(10):1740–1749

    Google Scholar 

  103. Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, New York

    Book  MATH  Google Scholar 

  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–162

    Article  Google Scholar 

  105. Marieb E, Hoehn K (2004) Human anatomy and physiology 2004. Daryl Fox, San Francisco

    Google Scholar 

  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–922

    Article  Google Scholar 

  107. Musi N, Goodyear LJ (2006) Insulin resistance and improvements in signal transduction. Endocrine 29(1):73–80

    Article  Google Scholar 

  108. Muske KR, Badgwell TA (2002) Disturbance modeling for offset-free linear model predictive control. J Process Control 12:617–632

    Article  Google Scholar 

  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–220

    Google Scholar 

  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–244

    Google Scholar 

  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 Congress

    Google Scholar 

  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–100

    Article  Google Scholar 

  113. Nucci G, Cobelli C (2000) Models of subcutaneous insulin kinetics. A critical review. Comput Methods Programs Biomed 62(3):249–257

    Article  Google Scholar 

  114. Otis B, Parviz B (2014) Introducing google’s smart contact lens project. Blog post on Google Inc. official weblog, http://googleblog.blogspot.com/2014/01/introducing-our-smart-contact-lens.html

  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–232

    Chapter  Google Scholar 

  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–2549

    Article  Google Scholar 

  117. Parker RS, Doyle FJ, Peppas NA (2001) The intravenous route to blood glucose control. IEEE Eng Med Biol Mag 20(1):65–73

    Article  Google Scholar 

  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–282

    Article  Google Scholar 

  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–88

    Article  Google Scholar 

  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–67

    Article  MathSciNet  MATH  Google Scholar 

  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–1142

    Article  Google Scholar 

  122. Platzer A (2008) Differential dynamic logic for hybrid systems. J Autom Reason 41(2):143–189

    Article  MathSciNet  MATH  Google Scholar 

  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–39

    Google Scholar 

  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–184

    Article  Google Scholar 

  125. Radcliffe J (2011) Hacking medical devices for fun and insulin: Breaking the human SCADA system. Black Hat 2011, Cf. https://media.blackhat.com/bh-us-11/Radcliffe/BH_US_11_Radcliffe_Hacking_Medical_Devices_WP.pdf

  126. Ramkissoon C, Aufderheide B, Bequette BW, Vehi J (2017) Safety and hazards associated with the artificial pancreas. IEEE Rev Biomed Eng 10:44–52

    Article  Google Scholar 

  127. Rawlings J, Mayne D, Diehl M (2017) Model predictive control: theory, computation and design. Nob Hill Publishing, Madison

    Google Scholar 

  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–2273

    Google Scholar 

  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–1130

    Article  Google Scholar 

  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:A98

    Article  Google Scholar 

  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. 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. https://doi.org/10.1007/978-3-319-70389-3_9, https://link.springer.com/chapter/10.1007%2F978-3-319-70389-3_9

    Chapter  Google Scholar 

  133. Siper MJ (2005) An introduction to mathematical theory of computation, 2nd edn. Thompson Publishing (Course Technology)

    Google Scholar 

  134. Skyler JS (ed) (2012) Atlas of Diabetes, 4th edn. Springer Science + Business Media

    Google Scholar 

  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. https://doi.org/10.2337/dc16-1794

    Article  Google Scholar 

  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–165

    Article  Google Scholar 

  137. Steil GM (2013) Algorithms for a closed-loop artificial pancreas: The case for proportional-integral-derivative control. J Diabetes Sci Technol 7:1621–1631

    Article  Google Scholar 

  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–144

    Article  Google Scholar 

  139. Turksoy K, Cinar A (2018) Multi-module multivariable artificial pancreas for patients with type 1 diabetes. IEEE Control Syst Mag 38(1):105–124

    Article  Google Scholar 

  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–400

    Article  Google Scholar 

  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. https://doi.org/10.1016/j.conengprac.2016.08.001

    Article  Google Scholar 

  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–1181

    Article  Google Scholar 

  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–939

    Article  Google Scholar 

  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 4

    Article  Google Scholar 

  145. Zavitsanou S, Chakrabarty A, Dassau E, Doyle FJ (2016) Embedded control in wearable medical devices: Application to the artificial pancreas. Processes 4(4)

    Article  Google Scholar 

Download references

Acknowledgements

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.

Author information

Authors and Affiliations

  1. University of Colorado, Boulder, CO, USA

    Taisa Kushner & Sriram Sankaranarayanan

  2. Rensselaer Polytechnic Institute, Troy, AL, USA

    B. Wayne Bequette & Faye Cameron

  3. Barbara Davis Center for Diabetes, University of Colorado Anschutz Medical Campus, Denver, CO, USA

    Gregory Forlenza

  4. Stanford University Medical Center, Stanford, CA, USA

    David Maahs

Authors
  1. Taisa Kushner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. B. Wayne Bequette
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Faye Cameron
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gregory Forlenza
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. David Maahs
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Sriram Sankaranarayanan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sriram Sankaranarayanan .

Editor information

Editors and Affiliations

  1. Department of Computer Science and Technology, University of Cambridge, Cambridge, UK

    Pietro Liò

  2. School of Computing, Newcastle University, Newcastle, UK

    Paolo Zuliani

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Kushner, T., Wayne Bequette, B., Cameron, F., Forlenza, G., Maahs, D., Sankaranarayanan, S. (2019). Models, Devices, Properties, and Verification of Artificial Pancreas Systems. In: Liò, P., Zuliani, P. (eds) Automated Reasoning for Systems Biology and Medicine. Computational Biology, vol 30. Springer, Cham. https://doi.org/10.1007/978-3-030-17297-8_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-17297-8_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-17296-1

  • Online ISBN: 978-3-030-17297-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation