{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T03:57:47Z","timestamp":1774324667684,"version":"3.50.1"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319238197","type":"print"},{"value":"9783319238203","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23820-3_1","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T14:21:39Z","timestamp":1442672499000},"page":"3-17","source":"Crossref","is-referenced-by-count":19,"title":["Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification"],"prefix":"10.1007","author":[{"given":"Fraser","family":"Cameron","sequence":"first","affiliation":[]},{"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[]},{"given":"David M.","family":"Maahs","sequence":"additional","affiliation":[]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,15]]},"reference":[{"key":"1_CR1","first-page":"95","volume":"12","author":"H Abbas","year":"2013","unstructured":"Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivancic, F.: Probabilistic temporal logic falsification of cyber-physical systems. Trans. Embedded Comput. Syst. (TECS) 12, 95 (2013)","journal-title":"Trans. Embedded Comput. Syst. (TECS)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Annapureddy, Y.S.R., Fainekos, G.E.: Ant colonies for temporal logic falsification of hybrid systems. In: Proceedings of the 36th Annual Conference of IEEE Industrial Electronics, pp. 91\u201396 (2010)","DOI":"10.1109\/IECON.2010.5675195"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254\u2013257. Springer, Heidelberg (2011)"},{"issue":"5","key":"1_CR4","doi-asserted-by":"crossref","first-page":"1072","DOI":"10.2337\/dc09-1830","volume":"33","author":"E Atlas","year":"2010","unstructured":"Atlas, E., Nimri, R., Miller, S., Grunberg, E.A., Phillip, M.: MD-Logic artificial pancreas system: a pilot study in adults with type 1 diabetes. Diabetes Care 33(5), 1072\u20131076 (2010)","journal-title":"Diabetes Care"},{"key":"1_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"11","key":"1_CR6","doi-asserted-by":"crossref","first-page":"2110","DOI":"10.2337\/dc08-0863","volume":"31","author":"B Buckingham","year":"2008","unstructured":"Buckingham, B., Wilson, D.M., Lecher, T., Hanas, R., Kaiserman, K., Cameron, F.: Duration of nocturnal hypoglycemia before seizures. Diabetes Care 31(11), 2110\u20132112 (2008)","journal-title":"Diabetes Care"},{"key":"1_CR7","unstructured":"Cameron, F.: Explicitly minimizing clinical risk through closed-loop control of blood glucose in patients with type 1 diabetes mellitus. Ph.D. thesis, Stanford University (2010)"},{"issue":"2","key":"1_CR8","doi-asserted-by":"crossref","first-page":"36879","DOI":"10.1177\/193229681100500226","volume":"5","author":"F Cameron","year":"2011","unstructured":"Cameron, F., Wayne Bequette, B., Wilson, D.M., Buckingham, B., Lee, H., Niemeyer, G.: Closed-loop artificial pancreas based on risk management. J. Diabetes Sci. Technol. 5(2), 36879 (2011)","journal-title":"J. Diabetes Sci. Technol."},{"issue":"8","key":"1_CR9","doi-asserted-by":"crossref","first-page":"1422","DOI":"10.1016\/j.jprocont.2012.05.014","volume":"22","author":"F Cameron","year":"2012","unstructured":"Cameron, F., Niemeyer, G., Wayne Bequette, B.: Extended multiple model prediction with application to blood glucose regulation. J. Process Control 22(8), 1422\u20131432 (2012)","journal-title":"J. Process Control"},{"issue":"5","key":"1_CR10","doi-asserted-by":"crossref","first-page":"1142","DOI":"10.1177\/193229681200600519","volume":"6","author":"F Cameron","year":"2012","unstructured":"Cameron, F., Wilson, D.M., Buckingham, B.A., Arzumanyan, H., Clinton, P., Peter Chase, H., Lum, J., Maahs, D.M., Calhoun, P.M.: Inpatient studies of a kalman-filter-based predictive pump shutoff algorithm. J. Diabetes Sci. Technol. 6(5), 1142\u20131147 (2012)","journal-title":"J. Diabetes Sci. Technol."},{"key":"1_CR11","volume-title":"Understanding Diabetes (Pink Panther Book)","author":"H Peter Chase","year":"2011","unstructured":"Peter Chase, H., Maahs, D.: Understanding Diabetes (Pink Panther Book), 12th edn. Children\u2019s Diabetes Foundation, Denver (2011). Available online through CU Denver Barbara Davis Center for Diabetes","edition":"12"},{"key":"1_CR12","volume-title":"Closed-Loop Control of Blood Glucose","author":"F Chee","year":"2007","unstructured":"Chee, F., Fernando, T.: Closed-Loop Control of Blood Glucose. Springer, Heidelberg (2007)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceeding of the RTSS 2012, pp. 183\u2013192. IEEE (2012)","DOI":"10.1109\/RTSS.2012.70"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","first-page":"258","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013)"},{"issue":"5","key":"1_CR15","doi-asserted-by":"crossref","first-page":"1212","DOI":"10.2337\/dc13-1631","volume":"37","author":"C Cobelli","year":"2014","unstructured":"Cobelli, C., et al.: First use of model predictive control in outpatient wearable artificial pancreas. Diabetes Care 37(5), 1212\u20131215 (2014)","journal-title":"Diabetes Care"},{"key":"1_CR16","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/RBME.2009.2036073","volume":"2","author":"C Cobelli","year":"2009","unstructured":"Cobelli, C., Dalla Man, C., Sparacino, G., Magni, L., De Nicolao, G., Kovatchev, B.P.: Diabetes: models, signals and control (methodological review). IEEE Rev. Biomed. Eng. 2, 54\u201395 (2009)","journal-title":"IEEE Rev. Biomed. Eng."},{"issue":"10","key":"1_CR17","first-page":"1740","volume":"1","author":"C Dall Man","year":"2006","unstructured":"Dall Man, C., Rizza, R.A., Cobelli, C.: Meal simulation model of the glucose-insulin system. IEEE Trans. Biomed. Eng. 1(10), 1740\u20131749 (2006)","journal-title":"IEEE Trans. Biomed. Eng."},{"issue":"2","key":"1_CR18","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/s10703-009-0066-0","volume":"34","author":"T Dang","year":"2009","unstructured":"Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods Syst. Des. 34(2), 183\u2013213 (2009)","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"1_CR19","doi-asserted-by":"crossref","first-page":"8019","DOI":"10.2337\/dc12-0948","volume":"36","author":"E Dassau","year":"2013","unstructured":"Dassau, E., Zisser, H., Harvey, R.A., Percival, M.W., Grosman, B., Bevier, W., Atlas, E., Miller, S., Nimri, R., Jovanovic, L., Doyle, F.J.: Clinical evaluation of a personalized artificial pancreas. Diabetes Care 36(4), 8019 (2013)","journal-title":"Diabetes Care"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/978-3-319-11164-3_19","volume-title":"Runtime Verification","author":"A Dokhanchi","year":"2014","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231\u2013246. Springer, Heidelberg (2014)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92\u2013106. Springer, Heidelberg (2010)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-319-17524-9_10","volume-title":"NASA Formal Methods","author":"T Dreossi","year":"2015","unstructured":"Dreossi, T., Dang, T., Donz\u00e9, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 127\u2013142. Springer, Heidelberg (2015)"},{"issue":"2","key":"1_CR25","doi-asserted-by":"crossref","first-page":"18192","DOI":"10.1177\/193229680700100208","volume":"1","author":"F El-Khatib","year":"2007","unstructured":"El-Khatib, F., Jiang, J., Damiano, E.R.: Adaptive closed-loop control provides blood-glucose regulation using dual subcutaneous insulin and glucagon infusion in diabetic swine. J. Diabetes Sci. Technol. 1(2), 18192 (2007)","journal-title":"J. Diabetes Sci. Technol."},{"key":"1_CR26","first-page":"27ra27","volume":"2","author":"FH El-Khatib","year":"2010","unstructured":"El-Khatib, F.H., Russell, S.J., Nathan, D.M., Sutherlin, R.G., Damiano, E.R.: A bihormonal closed-loop artificial panceras for type 1 diabetes. Sci. Transl. Med. 2, 27ra27 (2010)","journal-title":"Sci. Transl. Med."},{"key":"1_CR27","doi-asserted-by":"crossref","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"G Fainekos","year":"2009","unstructured":"Fainekos, G., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410, 4262\u20134291 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Fainekos, G., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using s-taliro. In: Proceedings of the American Control Conference (2012)","DOI":"10.1109\/ACC.2012.6315384"},{"issue":"5","key":"1_CR29","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1089\/dia.2015.0055","volume":"17","author":"GP Forlenza","year":"2015","unstructured":"Forlenza, G.P., Sankaranarayanan, S., Maahs, D.M.: Refining the closed loop in the data age: research-to-practice transitions in diabetes technology. Diabetes Technol. Ther. 17(5), 304\u2013306 (2015)","journal-title":"Diabetes Technol. Ther."},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G 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.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT Solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013)"},{"issue":"4","key":"1_CR32","doi-asserted-by":"crossref","first-page":"961","DOI":"10.1177\/193229681000400428","volume":"4","author":"B Grosman","year":"2010","unstructured":"Grosman, B., Dassau, E., Zisser, H.C., Jovanovic, L., Doyle, F.J.: Zone model predictive control: a strategy to minimize hyper- and hypoglycemic events. J. Diabetes Sci. Technol. 4(4), 961\u2013975 (2010)","journal-title":"J. Diabetes Sci. Technol."},{"key":"1_CR33","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1016\/S0140-6736(09)61998-X","volume":"375","author":"R Hovorka","year":"2010","unstructured":"Hovorka, R., Allen, J.M., Elleri, D., Chassin, L.J., Harris, J., Xing, D., Kollman, C., Hovorka, T., Larsen, A.M., Nodale, M., De Palma, A., Wilinska, M., Acerini, C., Dunger, D.: Manual closed-loop delivery in children and adoloscents with type 1 diabetes: a phase 2 randomised crossover trial. Lancet 375, 743\u2013751 (2010)","journal-title":"Lancet"},{"key":"1_CR34","doi-asserted-by":"crossref","first-page":"905","DOI":"10.1088\/0967-3334\/25\/4\/010","volume":"25","author":"R Hovorka","year":"2004","unstructured":"Hovorka, R., Canonico, V., Chassin, L.J., Haueter, U., Massi-Benedetti, M., Frederici, M.O., Pieber, T.R., Shaller, H.C., Schaupp, L., Vering, T., Wilinska, M.E.: Nonlinear model predictive control of glucose concentration in subjects with type 1 diabetes. Physiol. Measur. 25, 905\u2013920 (2004)","journal-title":"Physiol. Measur."},{"key":"1_CR35","doi-asserted-by":"crossref","first-page":"992","DOI":"10.1152\/ajpendo.00304.2001","volume":"282","author":"R Hovorka","year":"2002","unstructured":"Hovorka, R., Shojaee-Moradie, F., Carroll, P.V., Chassin, L.J., Gowrie, I.J., Jackson, N.C., Tudor, R.S., Umpleby, A.M., Hones, R.H.: Partitioning glucose distribution\/transport, disposal and endogenous production during IVGTT. Am. J. Physiol. Endocrinol. Metab. 282, 992\u20131007 (2002)","journal-title":"Am. J. Physiol. Endocrinol. Metab."},{"issue":"1","key":"1_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1111\/j.1464-5491.2005.01672.x","volume":"23","author":"R Hovorka","year":"2005","unstructured":"Hovorka, R.: Continuous glucose monitoring and closed-loop systems. Diabetic Med. 23(1), 1\u201312 (2005)","journal-title":"Diabetic Med."},{"key":"1_CR37","unstructured":"Hoxha, B., Bach, H., Abbas, H., Dokhanchi, A., Kobayashi, Y., Fainekos, G.: Towards formal specification visualization for testing and monitoring of cyber-physical systems. In: International Workshop on Design and Implementation of Formal Tools and Systems (2014)"},{"issue":"6","key":"1_CR38","doi-asserted-by":"crossref","first-page":"137481","DOI":"10.1177\/193229681000400611","volume":"4","author":"B Kovatchev","year":"2010","unstructured":"Kovatchev, B., Cobelli, C., Renard, E., Anderson, S., Breton, M., Patek, S., Clarke, W., Bruttomesso, D., Maran, A., Costa, S., Avogaro, A., Dalla Man, C., Facchinetti, A., Magni, L., De Nicolao, G., Place, J., Farret, A.: Multinational study of subcutaneous model-predictive closed-loop control in type 1 diabetes mellitus: summary of the results. J. Diabetes Sci. Technol. 4(6), 137481 (2010)","journal-title":"J. Diabetes Sci. Technol."},{"key":"1_CR39","doi-asserted-by":"crossref","first-page":"1036","DOI":"10.2337\/dc15-0364","volume":"38","author":"A Kowalski","year":"2015","unstructured":"Kowalski, A.: Pathway to artificial pancreas revisited: moving downstream. Diabetes Care 38, 1036\u20131043 (2015)","journal-title":"Diabetes Care"},{"issue":"4","key":"1_CR40","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"key":"1_CR41","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511546877","volume-title":"Planning Algorithms","author":"SM LaValle","year":"2006","unstructured":"LaValle, S.M.: Planning Algorithms. Cambridge University Press, New York (2006)"},{"issue":"8","key":"1_CR42","doi-asserted-by":"crossref","first-page":"658","DOI":"10.1089\/dia.2012.0053","volume":"14","author":"D Maahs","year":"2012","unstructured":"Maahs, D., Mayer-Davis, E., Bishop, F., Wang, L., Mangan, M., McMurray, R.G.: Outpatient assessment of determinants of glucose excursions in adolescents with type-1 diabetes. Diabetes Technol. Ther. 14(8), 658\u2013664 (2012)","journal-title":"Diabetes Technol. Ther."},{"issue":"5","key":"1_CR43","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1089\/dia.2013.0227","volume":"16","author":"DM Maahs","year":"2014","unstructured":"Maahs, D.M., Peter Chase, H., Westfall, E., Slover, R., Huang, S., Shin, J.J., Kaufman, F.R., Pyle, L., Snell-Bergeon, J.K.: The effects of lowering nighttime and breakfast glucose levels with sensor-augmented pump therapy on hemoglobin a1c levels in type 1 diabetes. Diabetes Technol. Ther. 16(5), 284\u2013291 (2014)","journal-title":"Diabetes Technol. Ther."},{"issue":"6","key":"1_CR44","doi-asserted-by":"crossref","first-page":"804","DOI":"10.1177\/193229680700100603","volume":"1","author":"L Magni","year":"2007","unstructured":"Magni, L., Raimondo, D.M., Bossi, L., Dalla Man, C., De Nicolao, G., Kovatchev, B., Cobelli, C.: Model predictive control of type 1 diabetes: an in silico trial. J. Diabetes Sci. Technol. 1(6), 804\u2013812 (2007)","journal-title":"J. Diabetes Sci. Technol."},{"issue":"12","key":"1_CR45","doi-asserted-by":"crossref","first-page":"2472","DOI":"10.1109\/TBME.2006.883792","volume":"53","author":"C DallaMan","year":"2006","unstructured":"DallaMan, C., Camilleri, M., Cobelli, C.: A system model of oral glucose absorption: validation on gold standard data. IEEE Trans. Biomed. Eng. 53(12), 2472\u20132478 (2006)","journal-title":"IEEE Trans. Biomed. Eng."},{"issue":"1","key":"1_CR46","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1177\/1932296813514502","volume":"8","author":"C Dalla Man","year":"2014","unstructured":"Dalla Man, C., Micheletto, F., Lv, D., Breton, M., Kovatchev, B., Cobelli, C.: The UVA\/PADOVA type 1 diabetes simulator: new features. J. Diabetes Sci. Technol. 8(1), 26\u201334 (2014)","journal-title":"J. Diabetes Sci. Technol."},{"issue":"3","key":"1_CR47","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1177\/193229680700100303","volume":"1","author":"C DallaMan","year":"2007","unstructured":"DallaMan, C., Raimondo, D.M., Rizza, R.A., Cobelli, C.: GIM, simulation software of meal glucose-insulin model. J. Diabetes Sci. Tech. 1(3), 323\u2013330 (2007)","journal-title":"J. Diabetes Sci. Tech."},{"key":"1_CR48","unstructured":"Medtronic Inc. \u201cparadigm\u201d insulin pump with low glucose suspend system (2012). http:\/\/www.medtronicdiabetes.ca\/en\/paradigm_veo_glucose.html"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivan\u010di\u0107, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Hybrid Systems: Computation and Control, pp. 211\u2013220. ACM Press (2010)","DOI":"10.1145\/1755952.1755983"},{"issue":"2","key":"1_CR50","doi-asserted-by":"crossref","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.A., Danne, T., Battelino, T., Phillip, M.: 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 (2014)","journal-title":"Pediatr. Diabetes"},{"issue":"2","key":"1_CR51","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1016\/j.cmpb.2010.06.007","volume":"102","author":"CC Palerm","year":"2011","unstructured":"Palerm, C.C.: Physiologic insulin delivery with insulin feedback: a control systems perspective. Comput. Methods Programs Biomed. 102(2), 130\u2013137 (2011)","journal-title":"Comput. Methods Programs Biomed."},{"issue":"2","key":"1_CR52","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1177\/193229680900300207","volume":"3","author":"SD Patek","year":"2009","unstructured":"Patek, S.D., Bequette, B.W., Breton, M., Buckingham, B.A., Dassau, E., Doyle III, F.J., Lum, J., Magni, L., Zisser, H.: 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 (2009)","journal-title":"J Diabetes Sci. Technol."},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/978-3-642-00768-2_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Plaku","year":"2009","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of LTL safety properties in hybrid systems. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 368\u2013382. Springer, Heidelberg (2009)"},{"key":"1_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/978-3-540-73368-3_48","volume-title":"Computer Aided Verification","author":"E Plaku","year":"2007","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 463\u2013476. Springer, Heidelberg (2007)"},{"issue":"4","key":"1_CR55","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s10009-012-0233-2","volume":"15","author":"E Plaku","year":"2013","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of ltl safety properties in hybrid systems. Int. J. Softw. Tools Technol. Transf. 15(4), 305\u2013320 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR56","series-title":"Lecture Notes in Computer Science (Lecture Notes in Bioinformatics)","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-540-88562-7_19","volume-title":"Computational Methods in Systems Biology","author":"A Rizk","year":"2008","unstructured":"Rizk, A., Batt, G., Fages, F., Soliman, S.: On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 251\u2013268. Springer, Heidelberg (2008)"},{"key":"1_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/978-3-642-33636-2_19","volume-title":"Computational Methods in Systems Biology","author":"S Sankaranarayanan","year":"2012","unstructured":"Sankaranarayanan, S., Fainekos, G.: Simulating insulin infusion pump risks by In-Silico modeling of the insulin-glucose regulatory system. In: Gilbert, D., Heiner, M. (eds.) CMSB 2012. LNCS, vol. 7605, pp. 322\u2013341. Springer, Heidelberg (2012)"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Fainekos, G.E.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: HSCC, pp. 125\u2013134. ACM (2012)","DOI":"10.1145\/2185632.2185653"},{"key":"1_CR59","volume-title":"Atlas of Diabetes","year":"2012","unstructured":"Skyler, J.S. (ed.): Atlas of Diabetes, 4th edn. Springer Science+Business Media, New York (2012)","edition":"4"},{"key":"1_CR60","doi-asserted-by":"crossref","first-page":"1621","DOI":"10.1177\/193229681300700623","volume":"7","author":"GM Steil","year":"2013","unstructured":"Steil, G.M.: Algorithms for a closed-loop artificial pancreas: the case for proportional-integral-derivative control. J. Diabetes Sci. Technol. 7, 1621\u20131631 (2013)","journal-title":"J. Diabetes Sci. Technol."},{"issue":"2","key":"1_CR61","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.addr.2003.08.011","volume":"56","author":"GM Steil","year":"2004","unstructured":"Steil, G.M., Panteleon, A.E., Rebrin, K.: Closed-loop insulin delivery - the path to physiological glucose control. Adv. Drug Delivery Rev. 56(2), 125\u2013144 (2004)","journal-title":"Adv. Drug Delivery Rev."},{"key":"1_CR62","doi-asserted-by":"crossref","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.: 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 (2008)","journal-title":"Diabetes Care"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23820-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,30]],"date-time":"2019-08-30T19:48:13Z","timestamp":1567194493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-23820-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319238197","9783319238203"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23820-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}