{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,29]],"date-time":"2025-12-29T11:34:58Z","timestamp":1767008098484},"publisher-location":"Cham","reference-count":145,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030172961"},{"type":"electronic","value":"9783030172978"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17297-8_4","type":"book-chapter","created":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T09:04:12Z","timestamp":1560243852000},"page":"93-131","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Models, Devices, Properties, and Verification of Artificial Pancreas Systems"],"prefix":"10.1007","author":[{"given":"Taisa","family":"Kushner","sequence":"first","affiliation":[]},{"given":"B.","family":"Wayne Bequette","sequence":"additional","affiliation":[]},{"given":"Faye","family":"Cameron","sequence":"additional","affiliation":[]},{"given":"Gregory","family":"Forlenza","sequence":"additional","affiliation":[]},{"given":"David","family":"Maahs","sequence":"additional","affiliation":[]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,6,12]]},"reference":[{"key":"4_CR1","first-page":"95","volume":"12","author":"H Abbas","year":"2013","unstructured":"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","journal-title":"Trans Embed Comput Syst (TECS)"},{"key":"4_CR2","unstructured":"Advisory R (2016) R7-2016-07: Multiple vulnerabilities in animas onetouch ping insulin pump. Cf. \n                    https:\/\/community.rapid7.com\/community\/infosec\/blog\/2016\/10\/04\/r7-2016-07-multiple-vulnerabilities-in-animas-onetouch-ping-insulin-pump"},{"issue":"6","key":"4_CR3","doi-asserted-by":"publisher","first-page":"716","DOI":"10.1109\/TAC.1974.1100705","volume":"19","author":"H. Akaike","year":"1974","unstructured":"Akaike H (1974) A new look at the statistical model identification. IEEE Trans Autom Control 19(6):716\u2013723","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"7","key":"4_CR4","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1002\/(SICI)1096-9136(199807)15:7<539::AID-DIA668>3.0.CO;2-S","volume":"15","author":"K.G.M.M. Alberti","year":"1998","unstructured":"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\u2013553","journal-title":"Diabetic Medicine"},{"key":"4_CR5","doi-asserted-by":"publisher","DOI":"10.1201\/9780203833445","volume-title":"Molecular Biology of the Cell","author":"Bruce Alberts","year":"2007","unstructured":"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"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"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\u2013257","DOI":"10.1007\/978-3-642-19835-9_21"},{"issue":"5","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1072","DOI":"10.2337\/dc09-1830","volume":"33","author":"E Atlas","year":"2010","unstructured":"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\u20131076","journal-title":"Diabetes Care"},{"key":"4_CR8","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge"},{"issue":"1","key":"4_CR9","doi-asserted-by":"publisher","first-page":"E55","DOI":"10.1152\/ajpendo.00190.2001","volume":"284","author":"R Basu","year":"2003","unstructured":"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\u2013E69","journal-title":"Am J Physiol-Endocrinol Metab"},{"issue":"6","key":"4_CR10","doi-asserted-by":"publisher","first-page":"1091","DOI":"10.1177\/1932296814553267","volume":"8","author":"N Baysal","year":"2014","unstructured":"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\u20131096","journal-title":"J Diabetes Sci Technol"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"1632","DOI":"10.1177\/193229681300700624","volume":"7","author":"BW Bequette","year":"2013","unstructured":"Bequette BW (2013) Algorithms for a closed-loop artificial pancreas: The case for model predictive control. J Diabetes Sci Technol 7:1632\u20131643","journal-title":"J Diabetes Sci Technol"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"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\u2013134. \n                    https:\/\/doi.org\/10.1109\/MCS.2017.2767119","DOI":"10.1109\/MCS.2017.2767119"},{"issue":"3","key":"4_CR13","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1159\/000089312","volume":"64","author":"Richard N. Bergman","year":"2005","unstructured":"Bergman RN (2005) Minimal model: Perspective from 2005. Hormone research, pp 8\u201315. \n                    https:\/\/doi.org\/10.1159\/000089312","journal-title":"Hormone Research in Paediatrics"},{"issue":"6","key":"4_CR14","doi-asserted-by":"publisher","first-page":"1489","DOI":"10.2337\/db07-9903","volume":"56","author":"RN Bergman","year":"2007","unstructured":"Bergman RN (2007) Orchestration of glucose homeostasis: From a small acorn to the california oak. Diabetes 56(6):1489\u20131501","journal-title":"Diabetes"},{"key":"4_CR15","first-page":"583","volume":"27","author":"RN Bergman","year":"1971","unstructured":"Bergman RN, Urquhart J (1971) The pilot gland approach to the study of insulin secretory dynamics. Recent Prog Horm Res 27:583\u2013605","journal-title":"Recent Prog Horm Res"},{"issue":"6","key":"4_CR16","doi-asserted-by":"publisher","first-page":"E667","DOI":"10.1152\/ajpendo.1979.236.6.E667","volume":"236","author":"RN Bergman","year":"1979","unstructured":"Bergman RN, Ider YZ, Bowden CR, Cobelli C (1979) Quantitative estimation of insulin sensitivity. Am J Physiol-Endocrinol Metab 236(6):E667","journal-title":"Am J Physiol-Endocrinol Metab"},{"issue":"2","key":"4_CR17","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s10107-017-1125-8","volume":"167","author":"D Bertsimas","year":"2018","unstructured":"Bertsimas D, Gupta V, Kallus N (2018) Data-driven robust optimization. Math. Program 167(2):235\u2013292","journal-title":"Program"},{"issue":"5","key":"4_CR18","doi-asserted-by":"publisher","first-page":"783","DOI":"10.1152\/jappl.1961.16.5.783","volume":"16","author":"VW Bolie","year":"1961","unstructured":"Bolie VW (1961) Coefficients of normal blood glucose regulation. J Appl Physiol 16(5):783\u2013788","journal-title":"J Appl Physiol"},{"issue":"4","key":"4_CR19","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/MCS.2017.2696759","volume":"37","author":"A Borri","year":"2017","unstructured":"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\u201349","journal-title":"IEEE Control Syst"},{"issue":"2","key":"4_CR20","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1177\/193229681100500226","volume":"5","author":"F Cameron","year":"2011","unstructured":"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\u2013379","journal-title":"J Diabetes Sci Technol"},{"issue":"8","key":"4_CR21","doi-asserted-by":"publisher","first-page":"1422","DOI":"10.1016\/j.jprocont.2012.05.014","volume":"22","author":"F Cameron","year":"2012","unstructured":"Cameron F, Niemeyer G, Bequette BW (2012) Extended multiple model prediction with application to blood glucose regulation. J Process Control 22(8):1422\u20131432","journal-title":"J Process Control"},{"issue":"5","key":"4_CR22","doi-asserted-by":"publisher","first-page":"1142","DOI":"10.1177\/193229681200600519","volume":"6","author":"F Cameron","year":"2012","unstructured":"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\u20131147","journal-title":"J Diabetes Sci Technol"},{"issue":"11","key":"4_CR23","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1089\/dia.2014.0093","volume":"16","author":"Fraser Cameron","year":"2014","unstructured":"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\u2013734. \n                    https:\/\/doi.org\/10.1089\/dia.2014.0093","journal-title":"Diabetes Technology & Therapeutics"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-23820-3_1","volume-title":"Runtime Verification","author":"Fraser Cameron","year":"2015","unstructured":"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\u201317"},{"issue":"9","key":"4_CR25","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1089\/dia.2017.0078","volume":"19","author":"FM Cameron","year":"2017","unstructured":"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\u2013532. \n                    https:\/\/doi.org\/10.1089\/dia.2017.0078","journal-title":"Diabetes Technol Ther"},{"key":"4_CR26","unstructured":"Chase HP, Maahs D (2011) Understanding diabetes (Pink Panther Book). Children\u2019s diabetes foundation, 12 edn. Available online through CU Denver Barbara Davis Center for Diabetes"},{"key":"4_CR27","volume-title":"Closed-loop control of blood glucose","author":"F Chee","year":"2007","unstructured":"Chee F, Fernando T (2007) Closed-loop control of blood glucose. Springer, Berlin"},{"key":"4_CR28","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"Xin Chen","year":"2013","unstructured":"Chen X, \u00c1brah\u00e1m E, Sankaranarayanan S (2013) Flow*: An analyzer for non-linear hybrid systems. In: Proceedings of CAV 2013, vol 8044. LNCS. Springer, Berlin, pp 258\u2013263"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Chen S, O\u2019Kelly 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)","DOI":"10.1016\/j.ifacol.2015.11.177"},{"key":"4_CR30","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge"},{"issue":"5","key":"4_CR31","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1177\/193229680900300506","volume":"3","author":"WL Clarke","year":"2009","unstructured":"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\u20131038","journal-title":"J Diabetes Sci Technol"},{"key":"4_CR32","volume-title":"Tracer kinetics in biomedical research","author":"C Cobelli","year":"2000","unstructured":"Cobelli C, Foster D, Toffolo G (2000) Tracer kinetics in biomedical research. Springer Science & Business Media, Berlin"},{"key":"4_CR33","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/RBME.2009.2036073","volume":"2","author":"C Cobelli","year":"2009","unstructured":"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\u201395","journal-title":"IEEE Rev Biomed Eng"},{"issue":"11","key":"4_CR34","doi-asserted-by":"publisher","first-page":"2672","DOI":"10.2337\/db11-0654","volume":"60","author":"C Cobelli","year":"2011","unstructured":"Cobelli C, Renard E, Kovatchev B (2011) Artificial pancreas: Past, present, future. Diabetes Care 60(11):2672\u20132682","journal-title":"Diabetes Care"},{"issue":"5","key":"4_CR35","doi-asserted-by":"publisher","first-page":"1212","DOI":"10.2337\/dc13-1631","volume":"37","author":"Simone Del Favero","year":"2014","unstructured":"Cobelli C et\u00a0al (2014) AP@Home Consortium. First use of model predictive control in outpatient wearable artificial pancreas. Diabetes Care 37(5):1212\u20131215","journal-title":"Diabetes Care"},{"issue":"2","key":"4_CR36","doi-asserted-by":"publisher","first-page":"904","DOI":"10.1002\/oca.2388","volume":"39","author":"DA Copp","year":"2018","unstructured":"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\u2013918","journal-title":"Optim Control Appl Methods"},{"issue":"4","key":"4_CR37","doi-asserted-by":"publisher","first-page":"868","DOI":"10.1172\/JCI31669","volume":"117","author":"PE Cryer","year":"2007","unstructured":"Cryer PE (2007) Hypoglycemia, functional brain failure, and brain death. J Clin Investig 117(4):868\u2013870","journal-title":"J Clin Investig"},{"key":"4_CR38","unstructured":"Cutler C, Ramaker B (1980) Dynamic matrix control a computer control algorithm. In: Proceedings of the joint automatic control conference. Paper WP5-B"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"de Moura LM, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: TACAS, vol 4963. LNCS. Springer, Berlin, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Diwakaran R, Sankaranarayanan S, Trivedi A (2017) Analyzing neighbourhoods of falsifying traces. In: International conference on CPS (to appear)","DOI":"10.1145\/3055004.3055029"},{"issue":"3","key":"4_CR41","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s10484-012-9194-1","volume":"37","author":"Y Dong","year":"2012","unstructured":"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\u2013215","journal-title":"Appl Psychophysiol Biofeedback"},{"key":"4_CR42","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"Alexandre Donz\u00e9","year":"2010","unstructured":"Donz\u00e9 A (2010) Breach: A toolbox for verification and parameter synthesis of hybrid systems. In: CAV, vol 6174. Lecture notes in computer science. Springer, Berlin"},{"key":"4_CR43","first-page":"92","volume-title":"Lecture Notes in Computer Science","author":"Alexandre Donz\u00e9","year":"2010","unstructured":"Donz\u00e9 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\u2013106"},{"key":"4_CR44","doi-asserted-by":"publisher","first-page":"1191","DOI":"10.2337\/dc13-2108","volume":"37","author":"FJ Doyle","year":"2014","unstructured":"Doyle FJ, Huyett LM, Lee JB, Zisser HC, Dassau E (2014) Closed-loop artificial pancreas systems: Engineering the algorithms. Diabetes Care 37:1191\u20131197","journal-title":"Diabetes Care"},{"issue":"3","key":"4_CR45","first-page":"942","volume":"81","author":"A Dunaif","year":"1996","unstructured":"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\u2013947","journal-title":"J Clin Endocrinol Metab"},{"key":"4_CR46","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-99429-1_11","volume-title":"Computational Methods in Systems Biology","author":"Souradeep Dutta","year":"2018","unstructured":"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\u2013202"},{"issue":"27","key":"4_CR47","doi-asserted-by":"publisher","first-page":"27ra27","DOI":"10.1126\/scitranslmed.3000619","volume":"2","author":"F. H. El-Khatib","year":"2010","unstructured":"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","journal-title":"Science Translational Medicine"},{"issue":"1","key":"4_CR48","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1177\/193229681000400102","volume":"4","author":"Andrea Facchinetti","year":"2010","unstructured":"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)","journal-title":"Journal of Diabetes Science and Technology"},{"key":"4_CR49","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"G Fainekos","year":"2009","unstructured":"Fainekos G, Pappas GJ (2009) Robustness of temporal logic specifications for continuous-time signals. Theor Comput Sci 410:4262\u20134291","journal-title":"Theor Comput Sci"},{"key":"4_CR50","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1089\/dia.2017.0424","volume":"20","author":"G Forlenza","year":"2018","unstructured":"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. \n                    https:\/\/doi.org\/10.1089\/dia.2017.0424","journal-title":"Diabetes Technol Ther"},{"key":"4_CR51","doi-asserted-by":"publisher","first-page":"1096","DOI":"10.2337\/dc17-0500","volume":"40","author":"G Forlenza","year":"2017","unstructured":"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\u20131102. \n                    https:\/\/doi.org\/10.2337\/dc17-0500","journal-title":"Diabetes Care"},{"issue":"8","key":"4_CR52","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1093\/comjnl\/41.8.578","volume":"41","author":"C Fraley","year":"1998","unstructured":"Fraley C, Raftery AE (1998) How many clusters? which clustering method? answers via model-based cluster analysis. Comput J 41(8):578\u2013588","journal-title":"Comput J"},{"key":"4_CR53","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"Goran Frehse","year":"2011","unstructured":"Frehse G, Le Guernic C, Donz\u00e9 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\u2013395"},{"key":"4_CR54","doi-asserted-by":"crossref","unstructured":"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\u2013214","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"4_CR55","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1080\/00986448608911397","volume":"46","author":"G Garcia","year":"1986","unstructured":"Garcia G, Morshedi A (1986) Quadratic programming solution of dynamic matrix control (QDMC). Chem Eng Commun 46:73\u201387","journal-title":"Chem Eng Commun"},{"issue":"3","key":"4_CR56","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1089\/dia.2016.0421","volume":"19","author":"Satish K. Garg","year":"2017","unstructured":"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\u20139","journal-title":"Diabetes Technology & Therapeutics"},{"key":"4_CR57","doi-asserted-by":"crossref","unstructured":"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\u20132892","DOI":"10.1109\/EMBC.2012.6346567"},{"issue":"1","key":"4_CR58","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1109\/TITB.2012.2219876","volume":"17","author":"EI Georga","year":"2013","unstructured":"Georga EI, Protopappas VC, Ardig\u00f2 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\u201381","journal-title":"IEEE J Biomed Health Inform"},{"key":"4_CR59","doi-asserted-by":"crossref","unstructured":"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\u20134842","DOI":"10.1109\/EMBC.2014.6944707"},{"key":"4_CR60","doi-asserted-by":"crossref","unstructured":"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\u2013315","DOI":"10.1109\/CDC.2014.7039399"},{"key":"4_CR61","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/j.automatica.2016.04.015","volume":"71","author":"R Gondhalekar","year":"2016","unstructured":"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\u2013246","journal-title":"Automatica"},{"issue":"1","key":"4_CR62","doi-asserted-by":"publisher","first-page":"11023","DOI":"10.1016\/j.ifacol.2017.08.2482","volume":"50","author":"L Griva","year":"2017","unstructured":"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\u201311028","journal-title":"IFAC-PapersOnLine"},{"issue":"4","key":"4_CR63","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1177\/193229681000400428","volume":"4","author":"B Grosman","year":"2010","unstructured":"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\u2013975","journal-title":"J Diabetes Sci Technol"},{"issue":"4","key":"4_CR64","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1177\/193229681000400428","volume":"4","author":"B Grosman","year":"2010","unstructured":"Grosman B, Dassau E, Zisser HC, Jovanovi\u010d L, Doyle FJ (2010b) Zone model predictive control: A strategy to minimize hyper- and hypoglycemic events. J Diabetes Sci Technol 4(4):961\u2013975","journal-title":"J Diabetes Sci Technol"},{"issue":"3","key":"4_CR65","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1089\/dia.2017.0333","volume":"20","author":"B Grosman","year":"2018","unstructured":"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\u2013221","journal-title":"Diabetes Technol Ther"},{"key":"4_CR66","unstructured":"Hakami H (Medtronic Inc.). FDA approves MINIMED 670G system - world\u2019s first hybrid closed loop system. \n                    https:\/\/www.medtronicdiabetes.com\/blog\/fda-approves-minimed-670g-system-worlds-first-hybrid-closed-loop-system\/"},{"issue":"2","key":"4_CR67","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/BF00547132","volume":"32","author":"DM Hamby","year":"1994","unstructured":"Hamby DM (1994) A review of techniques for parameter sensitivity analysis of environmental models. Environ Monit Assess 32(2):135\u2013154","journal-title":"Environ Monit Assess"},{"key":"4_CR68","unstructured":"HAPIfork. HAPIfork. \n                    https:\/\/www.hapi.com\/product\/hapifork\n                    \n                  . Accessed 26 Feb 2017"},{"key":"4_CR69","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1089\/dia.2013.0231","volume":"16","author":"R Harvey","year":"2014","unstructured":"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\u2013357","journal-title":"Diabetes Technol Ther"},{"issue":"1","key":"4_CR70","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1111\/j.1464-5491.2005.01672.x","volume":"23","author":"R Hovorka","year":"2005","unstructured":"Hovorka R (2005) Continuous glucose monitoring and closed-loop systems. Diabetic Med 23(1):1\u201312","journal-title":"Diabetic Med"},{"key":"4_CR71","doi-asserted-by":"publisher","first-page":"992","DOI":"10.1152\/ajpendo.00304.2001","volume":"282","author":"R Hovorka","year":"2002","unstructured":"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\u20131007","journal-title":"Am J Physiol Endocrinol Metab"},{"issue":"4","key":"4_CR72","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1088\/0967-3334\/25\/4\/010","volume":"25","author":"Roman Hovorka","year":"2004","unstructured":"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\u2013920","journal-title":"Physiological Measurement"},{"key":"4_CR73","doi-asserted-by":"publisher","unstructured":"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. \n                    https:\/\/doi.org\/10.1177\/19322968187551.Online","DOI":"10.1177\/19322968187551.Online"},{"issue":"12","key":"4_CR74","doi-asserted-by":"publisher","first-page":"161","DOI":"10.3390\/s17010161","volume":"17","author":"Daniel Howsmon","year":"2017","unstructured":"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. \n                    https:\/\/doi.org\/10.3390\/s17010161","journal-title":"Sensors"},{"issue":"5","key":"4_CR75","doi-asserted-by":"publisher","first-page":"1191","DOI":"10.2337\/dc13-2108","volume":"37","author":"FJD Iii","year":"2014","unstructured":"Iii FJD, Huyett LM, Lee JB, Zisser HC, Dassau E (2014) Closed-loop artificial pancreas systems: Engineering the algorithms. Diabetes Care 37(5):1191\u20131197","journal-title":"Diabetes Care"},{"issue":"6","key":"4_CR76","doi-asserted-by":"publisher","first-page":"1175","DOI":"10.1177\/1932296815609371","volume":"9","author":"PG Jacobs","year":"2015","unstructured":"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\u20131184","journal-title":"J Diabetes Sci Technol"},{"key":"4_CR77","doi-asserted-by":"crossref","unstructured":"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\u2013163","DOI":"10.1109\/DSDE.2010.58"},{"key":"4_CR78","doi-asserted-by":"crossref","unstructured":"Kissler SM, Cichowitz C, Sankaranarayanan S, Bortz DM (2014) Determination of personalized diabetes treatment plans using a two-delay model. J Theor Biol (accepted)","DOI":"10.1016\/j.jtbi.2014.06.005"},{"issue":"9","key":"4_CR79","doi-asserted-by":"publisher","first-page":"1121","DOI":"10.1016\/0026-0495(95)90003-9","volume":"44","author":"MT Korytkowski","year":"1995","unstructured":"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\u20131125","journal-title":"Metabolism"},{"key":"4_CR80","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1177\/193229680900300106"},{"key":"4_CR81","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.2337\/dc15-0364","volume":"38","author":"A Kowalski","year":"2015","unstructured":"Kowalski A (2015) Pathway to artificial pancreas revisited: Moving downstream. Diabetes Care 38:1036\u20131043","journal-title":"Diabetes Care"},{"issue":"4","key":"4_CR82","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255\u2013299","journal-title":"Real-Time Syst"},{"key":"4_CR83","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1109\/ICCPS.2018.00031"},{"issue":"1","key":"4_CR84","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1385\/ENDO:29:1:91","volume":"29","author":"J Kusunoki","year":"2006","unstructured":"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\u2013100","journal-title":"Endocrine"},{"issue":"4","key":"4_CR85","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1016\/j.bspc.2009.03.002","volume":"4","author":"H Lee","year":"2009","unstructured":"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\u2013354","journal-title":"Biomed Signal Process Control"},{"issue":"5","key":"4_CR86","doi-asserted-by":"publisher","first-page":"1082","DOI":"10.1177\/193229680900300511","volume":"3","author":"H Lee","year":"2009","unstructured":"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\u20131090","journal-title":"J Diabetes Sci Technol"},{"issue":"3","key":"4_CR87","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0141-5425(92)90058-S","volume":"14","author":"E Lehmann","year":"1992","unstructured":"Lehmann E, Deutsch T (1992) A physiological model of glucose-insulin interaction in type 1 diabetes mellitus. J Biomed Eng 14(3):235\u2013242","journal-title":"J Biomed Eng"},{"issue":"1","key":"4_CR88","doi-asserted-by":"publisher","first-page":"103","DOI":"10.3934\/dcdsb.2001.1.103","volume":"1","author":"J Li","year":"2001","unstructured":"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\u2013124","journal-title":"Discret Contin Dyn Syst Ser B"},{"issue":"3","key":"4_CR89","doi-asserted-by":"publisher","first-page":"722","DOI":"10.1016\/j.jtbi.2006.04.002","volume":"242","author":"J Li","year":"2006","unstructured":"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\u2013735","journal-title":"J Theor Biol"},{"key":"4_CR90","unstructured":"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\u2013156"},{"issue":"2","key":"4_CR91","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1038\/nprot.2014.025","volume":"9","author":"J Liepe","year":"2014","unstructured":"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\u2013456","journal-title":"Nat Protoc"},{"key":"4_CR92","doi-asserted-by":"crossref","unstructured":"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\u2013160","DOI":"10.1109\/BSN.2012.11"},{"issue":"2","key":"4_CR93","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.bspc.2012.09.003","volume":"8","author":"Katrin Lunze","year":"2013","unstructured":"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 \u2013 119. ISSN 1746\u20138094","journal-title":"Biomedical Signal Processing and Control"},{"issue":"7","key":"4_CR94","doi-asserted-by":"publisher","first-page":"1885","DOI":"10.2337\/dc13-2159","volume":"37","author":"David M. Maahs","year":"2014","unstructured":"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\u20131891","journal-title":"Diabetes Care"},{"key":"4_CR95","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/j.bspc.2018.09.012","volume":"48","author":"Z Mahmoudi","year":"2019","unstructured":"Mahmoudi Z, Cameron F, Poulsen NK, Madsen H, Bequette BW, J\u00f8rgensen JB (2019) Sensor-based detection and estimation of meal carbohydrates for people with diabetes. Biomed Signal Process Control 48:12\u201325","journal-title":"Biomed Signal Process Control"},{"issue":"3\u20134","key":"4_CR96","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1016\/j.apnum.2005.04.023","volume":"56","author":"A Makroglou","year":"2006","unstructured":"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\u20134):559\u2013573","journal-title":"Appl Numer Math"},{"key":"4_CR97","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"Oded Maler","year":"2004","unstructured":"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\u2013166"},{"key":"4_CR98","unstructured":"Man CD, Breton MD, Cobelli C (2009) Physical activity into the meal glucose-insulin model of type 1 diabetes: in silico studies"},{"issue":"12","key":"4_CR99","doi-asserted-by":"publisher","first-page":"2472","DOI":"10.1109\/TBME.2006.883792","volume":"53","author":"CD Man","year":"2006","unstructured":"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\u20132478","journal-title":"IEEE Trans Biomed Eng"},{"issue":"12","key":"4_CR100","doi-asserted-by":"publisher","first-page":"2472","DOI":"10.1109\/TBME.2006.883792","volume":"53","author":"C Man","year":"2006","unstructured":"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\u20132478","journal-title":"IEEE Trans Biomed Eng"},{"issue":"1","key":"4_CR101","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1177\/1932296813514502","volume":"8","author":"CD Man","year":"2014","unstructured":"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\u201334","journal-title":"J Diabetes Sci Technol"},{"issue":"10","key":"4_CR102","first-page":"1740","volume":"1","author":"CD Man","year":"2006","unstructured":"Man CD, Rizza RA, Cobelli C (2006) Meal simulation model of the glucose-insulin system. IEEE Trans Biomed Eng 1(10):1740\u20131749","journal-title":"IEEE Trans Biomed Eng"},{"key":"4_CR103","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems: safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, New York"},{"issue":"2","key":"4_CR104","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.jprocont.2007.07.008","volume":"18","author":"G Marchetti","year":"2008","unstructured":"Marchetti G, Barolo M, Jovanovi\u010d L, Zisser H, Seborg DE (2008) A feedforward-feedback glucose control strategy for type 1 diabetes mellitus. J Process Control 18(2):149\u2013162","journal-title":"J Process Control"},{"key":"4_CR105","volume-title":"Human anatomy and physiology 2004","author":"E Marieb","year":"2004","unstructured":"Marieb E, Hoehn K (2004) Human anatomy and physiology 2004. Daryl Fox, San Francisco"},{"issue":"4","key":"4_CR106","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1177\/193229681000400422","volume":"4","author":"Richard Mauseth","year":"2010","unstructured":"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\u2013922","journal-title":"Journal of Diabetes Science and Technology"},{"issue":"1","key":"4_CR107","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1385\/ENDO:29:1:73","volume":"29","author":"N Musi","year":"2006","unstructured":"Musi N, Goodyear LJ (2006) Insulin resistance and improvements in signal transduction. Endocrine 29(1):73\u201380","journal-title":"Endocrine"},{"key":"4_CR108","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1016\/S0959-1524(01)00051-8","volume":"12","author":"KR Muske","year":"2002","unstructured":"Muske KR, Badgwell TA (2002) Disturbance modeling for offset-free linear model predictive control. J Process Control 12:617\u2013632","journal-title":"J Process Control"},{"key":"4_CR109","doi-asserted-by":"crossref","unstructured":"Nghiem T, Sankaranarayanan S, Fainekos GE, Ivan\u010di\u0107 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\u2013220","DOI":"10.1145\/1755952.1755983"},{"key":"4_CR110","doi-asserted-by":"crossref","unstructured":"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\u2013244","DOI":"10.1145\/2994551.2994562"},{"key":"4_CR111","doi-asserted-by":"crossref","unstructured":"Nicolao GD, Magni L, Man CD, Cobelli C (2011) Modeling and control of diabetes: Towards the artificial pancreas. IFAC Proc Vol 44(1):7092 \u2013 7101. 18th IFAC World Congress","DOI":"10.3182\/20110828-6-IT-1002.03036"},{"issue":"2","key":"4_CR112","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1111\/pedi.12071","volume":"15","author":"R Nimri","year":"2014","unstructured":"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\u2013100","journal-title":"Pediatr Diabetes"},{"issue":"3","key":"4_CR113","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/S0169-2607(00)00071-7","volume":"62","author":"Gianluca Nucci","year":"2000","unstructured":"Nucci G, Cobelli C (2000) Models of subcutaneous insulin kinetics. A critical review. Comput Methods Programs Biomed 62(3):249\u2013257","journal-title":"Computer Methods and Programs in Biomedicine"},{"key":"4_CR114","unstructured":"Otis B, Parviz B (2014) Introducing google\u2019s smart contact lens project. Blog post on Google Inc. official weblog, \n                    http:\/\/googleblog.blogspot.com\/2014\/01\/introducing-our-smart-contact-lens.html"},{"key":"4_CR115","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-67471-1_13","volume-title":"Computational Methods in Systems Biology","author":"Nicola Paoletti","year":"2017","unstructured":"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\u2013232"},{"issue":"12","key":"4_CR116","doi-asserted-by":"publisher","first-page":"2537","DOI":"10.1002\/aic.690461220","volume":"46","author":"RS Parker","year":"2000","unstructured":"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\u20132549","journal-title":"AIChE J"},{"issue":"1","key":"4_CR117","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1109\/51.897829","volume":"20","author":"RS Parker","year":"2001","unstructured":"Parker RS, Doyle FJ, Peppas NA (2001) The intravenous route to blood glucose control. IEEE Eng Med Biol Mag 20(1):65\u201373","journal-title":"IEEE Eng Med Biol Mag"},{"issue":"2","key":"4_CR118","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1177\/193229680900300207","volume":"3","author":"S Patek","year":"2009","unstructured":"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\u2013282","journal-title":"J Diabetes Sci Technol"},{"issue":"1","key":"4_CR119","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1089\/dia.2009.0076","volume":"12","author":"C P\u00e9rez-Gand\u00eda","year":"2010","unstructured":"P\u00e9rez-Gand\u00eda C, Facchinetti A, Sparacino G, Cobelli C, G\u00f3mez 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\u201388","journal-title":"Diabetes Technol Ther"},{"issue":"1","key":"4_CR120","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0025-5564(03)00044-0","volume":"184","author":"G Pillonetto","year":"2003","unstructured":"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\u201367","journal-title":"Math Biosci"},{"issue":"7","key":"4_CR121","doi-asserted-by":"publisher","first-page":"1135","DOI":"10.2337\/dc15-2344","volume":"39","author":"JE Pinsker","year":"2016","unstructured":"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\u20131142","journal-title":"Diabetes Care"},{"issue":"2","key":"4_CR122","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer A (2008) Differential dynamic logic for hybrid systems. J Autom Reason 41(2):143\u2013189","journal-title":"J Autom Reason"},{"key":"4_CR123","first-page":"35","volume":"31","author":"K Plis","year":"2014","unstructured":"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\u201339","journal-title":"AAAI Work: Mod Artif Intell Health Anal"},{"issue":"3\u20134","key":"4_CR124","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1159\/000023168","volume":"49","author":"KS Polonsky","year":"1998","unstructured":"Polonsky KS, Sturis J, Van Cauter E (1998) Temporal profiles and clinical significance of pulsatile insulin secretion. Horm Res Paediatr 49(3\u20134):178\u2013184","journal-title":"Horm Res Paediatr"},{"key":"4_CR125","unstructured":"Radcliffe J (2011) Hacking medical devices for fun and insulin: Breaking the human SCADA system. Black Hat 2011, Cf. \n                    https:\/\/media.blackhat.com\/bh-us-11\/Radcliffe\/BH_US_11_Radcliffe_Hacking_Medical_Devices_WP.pdf"},{"key":"4_CR126","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/RBME.2017.2749038","volume":"10","author":"C Ramkissoon","year":"2017","unstructured":"Ramkissoon C, Aufderheide B, Bequette BW, Vehi J (2017) Safety and hazards associated with the artificial pancreas. IEEE Rev Biomed Eng 10:44\u201352","journal-title":"IEEE Rev Biomed Eng"},{"key":"4_CR127","volume-title":"Model predictive control: theory, computation and design","author":"J Rawlings","year":"2017","unstructured":"Rawlings J, Mayne D, Diehl M (2017) Model predictive control: theory, computation and design. Nob Hill Publishing, Madison"},{"key":"4_CR128","doi-asserted-by":"crossref","unstructured":"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\u20132273","DOI":"10.1109\/EMBC.2016.7591182"},{"issue":"5","key":"4_CR129","doi-asserted-by":"publisher","first-page":"1123","DOI":"10.1177\/193229681200600517","volume":"6","author":"JL Ruiz","year":"2012","unstructured":"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\u20131130","journal-title":"J Diabetes Sci Technol"},{"key":"4_CR130","doi-asserted-by":"publisher","first-page":"A98","DOI":"10.2337\/db06-S013","volume":"55","author":"MF Saad","year":"2006","unstructured":"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","journal-title":"Diabetes"},{"key":"4_CR131","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/3076125.3076128"},{"key":"4_CR132","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-70389-3_9","volume-title":"Hardware and Software: Verification and Testing","author":"Fedor Shmarov","year":"2017","unstructured":"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\u2013146. \n                    https:\/\/doi.org\/10.1007\/978-3-319-70389-3_9\n                    \n                  , \n                    https:\/\/link.springer.com\/chapter\/10.1007%2F978-3-319-70389-3_9"},{"key":"4_CR133","unstructured":"Siper MJ (2005) An introduction to mathematical theory of computation, 2nd edn. Thompson Publishing (Course Technology)"},{"key":"4_CR134","doi-asserted-by":"crossref","unstructured":"Skyler JS (ed) (2012) Atlas of Diabetes, 4th edn. Springer Science + Business Media","DOI":"10.1007\/978-1-4614-1028-7"},{"issue":"3","key":"4_CR135","doi-asserted-by":"publisher","first-page":"359","DOI":"10.2337\/dc16-1794","volume":"40","author":"Tamara Spaic","year":"2017","unstructured":"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\u2013366. \n                    https:\/\/doi.org\/10.2337\/dc16-1794","journal-title":"Diabetes Care"},{"issue":"2","key":"4_CR136","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1016\/0010-4809(70)90021-2","volume":"3","author":"R Srinivasan","year":"1970","unstructured":"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\u2013165","journal-title":"Comput Biomed Res"},{"key":"4_CR137","doi-asserted-by":"publisher","first-page":"1621","DOI":"10.1177\/193229681300700623","volume":"7","author":"GM Steil","year":"2013","unstructured":"Steil GM (2013) Algorithms for a closed-loop artificial pancreas: The case for proportional-integral-derivative control. J Diabetes Sci Technol 7:1621\u20131631","journal-title":"J Diabetes Sci Technol"},{"issue":"2","key":"4_CR138","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.addr.2003.08.011","volume":"56","author":"G Steil","year":"2004","unstructured":"Steil G, Panteleon A, Rebrin K (2004) Closed-sloop insulin delivery - the path to physiological glucose control. Adv Drug Deliv Rev 56(2):125\u2013144","journal-title":"Adv Drug Deliv Rev"},{"issue":"1","key":"4_CR139","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1109\/MCS.2017.2766326","volume":"38","author":"K Turksoy","year":"2018","unstructured":"Turksoy K, Cinar A (2018) Multi-module multivariable artificial pancreas for patients with type 1 diabetes. IEEE Control Syst Mag 38(1):105\u2013124","journal-title":"IEEE Control Syst Mag"},{"issue":"5","key":"4_CR140","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1089\/dia.2012.0283","volume":"15","author":"K Turksoy","year":"2013","unstructured":"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\u2013400","journal-title":"J Diabetes Technol Ther"},{"key":"4_CR141","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/j.conengprac.2016.08.001","volume":"59","author":"K Turksoy","year":"2017","unstructured":"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\u2013164. \n                    https:\/\/doi.org\/10.1016\/j.conengprac.2016.08.001","journal-title":"Control Eng Practice"},{"key":"4_CR142","doi-asserted-by":"publisher","first-page":"1174","DOI":"10.1177\/193229681000400516","volume":"4","author":"J Walsh","year":"2010","unstructured":"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\u20131181","journal-title":"J Diabetes Sci Technol"},{"key":"4_CR143","doi-asserted-by":"publisher","first-page":"934","DOI":"10.2337\/dc07-1967","volume":"31","author":"S Weinzimer","year":"2008","unstructured":"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\u2013939","journal-title":"Diabetes Care"},{"issue":"1","key":"4_CR144","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1177\/193229681000400117","volume":"4","author":"Malgorzata E. Wilinska","year":"2010","unstructured":"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","journal-title":"Journal of Diabetes Science and Technology"},{"issue":"4","key":"4_CR145","doi-asserted-by":"publisher","first-page":"35","DOI":"10.3390\/pr4040035","volume":"4","author":"Stamatina Zavitsanou","year":"2016","unstructured":"Zavitsanou S, Chakrabarty A, Dassau E, Doyle FJ (2016) Embedded control in wearable medical devices: Application to the artificial pancreas. Processes 4(4)","journal-title":"Processes"}],"container-title":["Computational Biology","Automated Reasoning for Systems Biology and Medicine"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17297-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T09:13:06Z","timestamp":1560244386000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17297-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030172961","9783030172978"],"references-count":145,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17297-8_4","relation":{},"ISSN":["1568-2684","2662-2432"],"issn-type":[{"type":"print","value":"1568-2684"},{"type":"electronic","value":"2662-2432"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}