{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:41Z","timestamp":1776316961030,"version":"3.50.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,3,31]],"date-time":"2017-03-31T00:00:00Z","timestamp":1490918400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGBED Rev."],"published-print":{"date-parts":[[2017,3,31]]},"abstract":"<jats:p>We present a model-based falsification scheme for artificial pancreas controllers. Our approach performs a closed-loop simulation of the control software using models of the human insulin-glucose regulatory system. Our work focuses on testing properties of an overnight control system for hypoglycemia\/hyperglycemia minimization in patients with type-1 diabetes. This control system is currently the subject of extensive phase II clinical trials.<\/jats:p>\n          <jats:p>We describe how the overall closed loop simulator is constructed, and formulate properties to be tested. Significantly, the closed loop simulation incorporates the control software, as is, without any abstractions. Next, we demonstrate the use of a simulation-based falsification approach to find potential property violations in the resulting control system. We formulate a series of properties about the controller behavior and examine the violations obtained. Using these violations, we propose modifications to the controller software to improve its performance under these adverse (corner-case) scenarios. We also illustrate the effectiveness of robustness as a metric for identifying interesting property violations. Finally, we identify important open problems for future work.<\/jats:p>","DOI":"10.1145\/3076125.3076128","type":"journal-article","created":{"date-parts":[[2017,4,3]],"date-time":"2017-04-03T12:13:39Z","timestamp":1491221619000},"page":"24-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Model-based falsification of an artificial pancreas control system"],"prefix":"10.1145","volume":"14","author":[{"given":"Sriram","family":"Sankaranarayanan","sequence":"first","affiliation":[{"name":"University of Colorado"}]},{"given":"Suhas Akshar","family":"Kumar","sequence":"additional","affiliation":[{"name":"University of Colorado"}]},{"given":"Faye","family":"Cameron","sequence":"additional","affiliation":[{"name":"Rensselaer Polytechnic Institute"}]},{"given":"B. Wayne","family":"Bequette","sequence":"additional","affiliation":[{"name":"Rensselaer Polytechnic Institute"}]},{"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[{"name":"Arizona State University"}]},{"given":"David M.","family":"Maahs","sequence":"additional","affiliation":[{"name":"University of Colorado"}]}],"member":"320","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Probabilistic temporal logic falsification of cyber-physical systems. Trans. on Embedded Computing Systems (TECS), 12:95-","author":"Abbas H.","year":"2013"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/IECON.2010.5675195"},{"key":"e_1_2_1_3_1","series-title":"LNCS","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":"Annapureddy Y. S. R.","year":"2011"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2337\/dc09-1830"},{"key":"e_1_2_1_5_1","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.02.046"},{"key":"e_1_2_1_7_1","first-page":"8","volume-title":"Hormone Research","author":"Bergman R. N.","year":"2005"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-571127-2.50039-0"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229681100500226"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23820-3_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jprocont.2012.05.014"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229681200600519"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229681000400127"},{"key":"e_1_2_1_15_1","volume-title":"Closed-Loop Control of Blood Glucose","author":"Chee F.","year":"2007"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2015.11.177"},{"key":"e_1_2_1_17_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2337\/dc13-1631"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/RBME.2009.2036073"},{"issue":"10","key":"e_1_2_1_20_1","first-page":"1740","article-title":"Meal simulation model of the glucose-insulin system","volume":"1","author":"Man C. Dalla","year":"2006","journal-title":"IEEE Transactions on Biomedical Engineering"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.2337\/dc12-0948"},{"key":"e_1_2_1_22_1","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":"FORMATS","author":"Donz\u00e9 A.","year":"2010"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229680700100208"},{"key":"e_1_2_1_24_1","volume-title":"Sci. Transl. Med.","author":"El-Khatib F. H.","year":"2010"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229681000400102"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_2_1_27_1","volume-title":"University of Pennsylvania","author":"Fainekos G. E.","year":"2008"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1089\/dia.2015.0055"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229681000400428"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1464-5491.2005.01672.x"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0140-6736(09)61998-X"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1088\/0967-3334\/25\/4\/010"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1152\/ajpendo.00304.2001"},{"key":"e_1_2_1_34_1","first-page":"1","volume-title":"International Journal on Software Tools for Technology Transfer","author":"Jiang Z.","year":"2013"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_14"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229681000400611"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.2337\/dc15-0364"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.2337\/dc13-2159"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229680700100603"},{"issue":"12","key":"e_1_2_1_41_1","first-page":"2472","article-title":"A system model of oral glucose absorption: Validation on gold standard data. Biomedical Engineering","volume":"53","author":"Man C. D.","year":"2006","journal-title":"IEEE Transactions on"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1177\/1932296813514502"},{"issue":"3","key":"e_1_2_1_43_1","article-title":"GIM, simulation software of meal glucose-insulin model","volume":"1","author":"Man C. D.","year":"2007","journal-title":"J. Diabetes Sci. and Tech."},{"key":"e_1_2_1_44_1","unstructured":"Medtronic Inc. \"paradigm\" insulin pump with low glucose suspend system 2012. Cf. http:\/\/www.medtronicdiabetes.ca\/en\/paradigm_veo_glucose.html.  Medtronic Inc. \"paradigm\" insulin pump with low glucose suspend system 2012. Cf. http:\/\/www.medtronicdiabetes.ca\/en\/paradigm_veo_glucose.html."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755952.1755983"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1111\/pedi.12071"},{"issue":"1","key":"e_1_2_1_47_1","first-page":"3","article-title":"Model-driven safety analysis of closed-loop medical systems. Industrial Informatics","volume":"10","author":"Pajic M.","year":"2014","journal-title":"IEEE Transactions on"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229680900300207"},{"key":"e_1_2_1_49_1","first-page":"216","volume-title":"Proc. Computational Methods in Systems Biology","author":"Pei Y.","year":"2005"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88562-7_19"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185632.2185653"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229681300700623"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229680800200115"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1177\/193229681000400117"}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3076125.3076128","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3076125.3076128","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:43Z","timestamp":1750215823000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3076125.3076128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,31]]},"references-count":53,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,3,31]]}},"alternative-id":["10.1145\/3076125.3076128"],"URL":"https:\/\/doi.org\/10.1145\/3076125.3076128","relation":{},"ISSN":["1551-3688"],"issn-type":[{"value":"1551-3688","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,31]]},"assertion":[{"value":"2017-03-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}