{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T07:56:50Z","timestamp":1780473410171,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,11,20]],"date-time":"2021-11-20T00:00:00Z","timestamp":1637366400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004541","name":"Ministry of Human Resource Development","doi-asserted-by":"publisher","award":["Government of India (SPARC P#701)"],"award-info":[{"award-number":["Government of India (SPARC P#701)"]}],"id":[{"id":"10.13039\/501100004541","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,20]]},"DOI":"10.1145\/3487212.3487342","type":"proceedings-article","created":{"date-parts":[[2021,12,21]],"date-time":"2021-12-21T20:01:45Z","timestamp":1640116905000},"page":"56-65","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A secure insulin infusion system using verification monitors"],"prefix":"10.1145","author":[{"given":"Abhinandan","family":"panda","sequence":"first","affiliation":[{"name":"IIT Bhubaneswar, Bhubaneswar, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Srinivas","family":"Pinisetty","sequence":"additional","affiliation":[{"name":"IIT Bhubaneswar, Bhubaneswar, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Partha","family":"Roop","sequence":"additional","affiliation":[{"name":"University of Auckland, Auckland, New Zealand"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,12,21]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Computers in Cardiology","author":"Alexakis C","year":"2003","unstructured":"C Alexakis , HO Nyongesa , R Saatchi , ND Harris , C Davies , C Emery , RH Ireland , and SR Heller . 2003. Feature extraction and classification of electrocardiogram (ECG) signals related to hypoglycaemia . In Computers in Cardiology , 2003 . IEEE , 537--540. C Alexakis, HO Nyongesa, R Saatchi, ND Harris, C Davies, C Emery, RH Ireland, and SR Heller. 2003. Feature extraction and classification of electrocardiogram (ECG) signals related to hypoglycaemia. In Computers in Cardiology, 2003. IEEE, 537--540."},{"key":"e_1_3_2_1_2_1","volume-title":"A knowledge-based electrocardiogram-monitoring system for detection of the onset of nocturnal hypoglycaemia in type 1 diabetic patients. In 2006 Computers in Cardiology","author":"Alexakis C","unstructured":"C Alexakis , Marcos Rodrigues , Reza Saatchi , HO Nyongesa , C Davies , RH Ireland , ND Harris , and SR Heller . 2006. A knowledge-based electrocardiogram-monitoring system for detection of the onset of nocturnal hypoglycaemia in type 1 diabetic patients. In 2006 Computers in Cardiology . IEEE , 5--8. C Alexakis, Marcos Rodrigues, Reza Saatchi, HO Nyongesa, C Davies, RH Ireland, ND Harris, and SR Heller. 2006. A knowledge-based electrocardiogram-monitoring system for detection of the onset of nocturnal hypoglycaemia in type 1 diabetic patients. In 2006 Computers in Cardiology. IEEE, 5--8."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10916-011-9739-5"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jacc.2018.01.023"},{"key":"e_1_3_2_1_5_1","volume-title":"Algorithms for monitoring real-time properties. Acta informatica 55, 4","author":"Basin David","year":"2018","unstructured":"David Basin , Felix Klaedtke , and Eugen Z\u0103linescu . 2018. Algorithms for monitoring real-time properties. Acta informatica 55, 4 ( 2018 ), 309--338. David Basin, Felix Klaedtke, and Eugen Z\u0103linescu. 2018. Algorithms for monitoring real-time properties. Acta informatica 55, 4 (2018), 309--338."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Xin Chen Souradeep Dutta and Sriram Sankaranarayanan. 2017. Formal Verification of a Multi-Basal Insulin Infusion Control Model.. In ARCH@ CPSWeek. 75--91. Xin Chen Souradeep Dutta and Sriram Sankaranarayanan. 2017. Formal Verification of a Multi-Basal Insulin Infusion Control Model.. In ARCH@ CPSWeek. 75--91.","DOI":"10.29007\/kcrp"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00125-010-1802-0"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.347.6221.499"},{"key":"e_1_3_2_1_10_1","unstructured":"Gari D Clifford Francisco Azuaje Patrick McSharry etal 2006. Advanced methods and tools for ECG data analysis. Artech house Boston. Gari D Clifford Francisco Azuaje Patrick McSharry et al. 2006. Advanced methods and tools for ECG data analysis. Artech house Boston."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04694-0_4"},{"key":"e_1_3_2_1_12_1","unstructured":"Andy Field. 2013. Discovering statistics using IBM SPSS statistics. sage. Andy Field. 2013. Discovering statistics using IBM SPSS statistics. sage."},{"key":"e_1_3_2_1_13_1","unstructured":"US Food Drug Administration etal 2010. White paper: Infusion pump improvement initiative. Food and Drug Administration Website (2010). US Food Drug Administration et al. 2010. White paper: Infusion pump improvement initiative. Food and Drug Administration Website (2010)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.31"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02637024"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"MK Islam G Tangim T Ahammad MRH Khondokar etal 2012. Study and analysis of ecg signal using matlab &labview as effective tools. International journal of Computer and Electrical engineering 4 3 (2012) 404. MK Islam G Tangim T Ahammad MRH Khondokar et al. 2012. Study and analysis of ecg signal using matlab &labview as effective tools. International journal of Computer and Electrical engineering 4 3 (2012) 404.","DOI":"10.7763\/IJCEE.2012.V4.522"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2337\/diab.39.12.1550"},{"key":"e_1_3_2_1_18_1","volume-title":"Patricia Beaston, Arleen Pinkos, Sally Y Choe, Guillermo Arreaza-Rub\u00edn, and William Heetderks.","author":"Klonoff David C","year":"2011","unstructured":"David C Klonoff , Charles L Zimliki , LCDR Alan Stevens , Patricia Beaston, Arleen Pinkos, Sally Y Choe, Guillermo Arreaza-Rub\u00edn, and William Heetderks. 2011 . Innovations in technology for the treatment of diabetes: clinical development of the artificial pancreas (an autonomous system). David C Klonoff, Charles L Zimliki, LCDR Alan Stevens, Patricia Beaston, Arleen Pinkos, Sally Y Choe, Guillermo Arreaza-Rub\u00edn, and William Heetderks. 2011. Innovations in technology for the treatment of diabetes: clinical development of the artificial pancreas (an autonomous system)."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMBC.2014.6944189"},{"key":"e_1_3_2_1_20_1","volume-title":"2011 IEEE 13th International Conference on e-Health Networking, Applications and Services. IEEE, 150--156","author":"Li Chunxiao","year":"2011","unstructured":"Chunxiao Li , Anand Raghunathan , and Niraj K Jha . 2011 . Hijacking an insulin pump: Security attacks and defenses for a diabetes therapy system . In 2011 IEEE 13th International Conference on e-Health Networking, Applications and Services. IEEE, 150--156 . Chunxiao Li, Anand Raghunathan, and Niraj K Jha. 2011. Hijacking an insulin pump: Security attacks and defenses for a diabetes therapy system. In 2011 IEEE 13th International Conference on e-Health Networking, Applications and Services. IEEE, 150--156."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001250051345"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2857705.2857746"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMBC.2012.6346525"},{"key":"e_1_3_2_1_24_1","volume-title":"SPSS: Statistical package for the social sciences.","author":"Nie Norman H","year":"1975","unstructured":"Norman H Nie , Dale H Bent , and C Hadlai Hull . 1975 . SPSS: Statistical package for the social sciences. Vol. 227 . McGraw-Hill New York . Norman H Nie, Dale H Bent, and C Hadlai Hull. 1975. SPSS: Statistical package for the social sciences. Vol. 227. McGraw-Hill New York."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/IEMBS.2010.5627430"},{"key":"e_1_3_2_1_26_1","volume-title":"Towards Certified Runtime Verification. In ICFEM 2012 (LNCS)","volume":"7635","author":"Blech Jan Olaf","year":"2012","unstructured":"Jan Olaf Blech , Yli\u00e8s Falcone , and Klaus Becker . 2012 . Towards Certified Runtime Verification. In ICFEM 2012 (LNCS) , Vol. 7635 . Springer, 494--509. Jan Olaf Blech, Yli\u00e8s Falcone, and Klaus Becker. 2012. Towards Certified Runtime Verification. In ICFEM 2012 (LNCS), Vol. 7635. Springer, 494--509."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TBME.1985.325532"},{"key":"e_1_3_2_1_28_1","volume-title":"Oak Ridge National Laboratory JDRF meeting.","author":"Paul Nathanael","year":"2010","unstructured":"Nathanael Paul . 2010 . Insulin pump security and reliability: Past, present, and future . In Oak Ridge National Laboratory JDRF meeting. Nathanael Paul. 2010. Insulin pump security and reliability: Past, present, and future. In Oak Ridge National Laboratory JDRF meeting."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2017.06.060"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556922"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Laurie Pycroft and Tipu Z Aziz. 2018. Security of implantable medical devices with wireless connections: The dangers of cyber-attacks. Laurie Pycroft and Tipu Z Aziz. 2018. Security of implantable medical devices with wireless connections: The dangers of cyber-attacks.","DOI":"10.1080\/17434440.2018.1483235"},{"key":"e_1_3_2_1_32_1","volume-title":"Black Hat Conference presentation slides","volume":"2011","author":"Radcliffe Jerome","year":"2011","unstructured":"Jerome Radcliffe . 2011 . Hacking medical devices for fun and insulin: Breaking the human SCADA system . In Black Hat Conference presentation slides , Vol. 2011 . Jerome Radcliffe. 2011. Hacking medical devices for fun and insulin: Breaking the human SCADA system. In Black Hat Conference presentation slides, Vol. 2011."},{"key":"e_1_3_2_1_33_1","volume-title":"Wall Street Journal [Internet]","author":"Rockoff JD","year":"2016","unstructured":"JD Rockoff . 2016. J& J Warned Insulin Pump Vulnerable to Cyber Hacking . Wall Street Journal [Internet] ( 2016 ). JD Rockoff. 2016. J&J Warned Insulin Pump Vulnerable to Cyber Hacking. Wall Street Journal [Internet] (2016)."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2667218"},{"key":"e_1_3_2_1_35_1","volume-title":"Association of hyperglycemia with reduced heart rate variability (The Framingham Heart Study). The American journal of cardiology 86, 3","author":"Singh Jagmeet P","year":"2000","unstructured":"Jagmeet P Singh , Martin G Larson , Christopher J O'Donnell , Peter F Wilson , Hisako Tsuji , Donald M Lloyd-Jones , and Daniel Levy . 2000. Association of hyperglycemia with reduced heart rate variability (The Framingham Heart Study). The American journal of cardiology 86, 3 ( 2000 ), 309--312. Jagmeet P Singh, Martin G Larson, Christopher J O'Donnell, Peter F Wilson, Hisako Tsuji, Donald M Lloyd-Jones, and Daniel Levy. 2000. Association of hyperglycemia with reduced heart rate variability (The Framingham Heart Study). The American journal of cardiology 86, 3 (2000), 309--312."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21070-4_39"},{"key":"e_1_3_2_1_37_1","volume-title":"Insulin pump hacker says vendor Medtronic is ignoring security risk. Venturebeat","author":"Takahashi D","year":"2011","unstructured":"D Takahashi . 2011. Insulin pump hacker says vendor Medtronic is ignoring security risk. Venturebeat ( 2011 ). https:\/\/venturebeat.com\/2011\/08\/25\/insulin-pump-hacker-says-vendor-medtronic-is-ignoring-security-risk\/ D Takahashi. 2011. Insulin pump hacker says vendor Medtronic is ignoring security risk. Venturebeat (2011). https:\/\/venturebeat.com\/2011\/08\/25\/insulin-pump-hacker-says-vendor-medtronic-is-ignoring-security-risk\/"},{"key":"e_1_3_2_1_38_1","volume-title":"Statistical and spectral analysis of ECG signal towards achieving non-invasive blood glucose monitoring. BMC medical informatics and decision making 19, 6","author":"Tobore Igbe","year":"2019","unstructured":"Igbe Tobore , Jingzhen Li , Abhishek Kandwal , Liu Yuhang , Zedong Nie , and Lei Wang . 2019. Statistical and spectral analysis of ECG signal towards achieving non-invasive blood glucose monitoring. BMC medical informatics and decision making 19, 6 ( 2019 ), 1--14. Igbe Tobore, Jingzhen Li, Abhishek Kandwal, Liu Yuhang, Zedong Nie, and Lei Wang. 2019. Statistical and spectral analysis of ECG signal towards achieving non-invasive blood glucose monitoring. BMC medical informatics and decision making 19, 6 (2019), 1--14."},{"key":"e_1_3_2_1_39_1","volume-title":"Diabetic ketoacidosis. American family physician 71, 9","author":"Trachtenbarg David E","year":"2005","unstructured":"David E Trachtenbarg . 2005. Diabetic ketoacidosis. American family physician 71, 9 ( 2005 ), 1705--1714. David E Trachtenbarg. 2005. Diabetic ketoacidosis. American family physician 71, 9 (2005), 1705--1714."},{"key":"e_1_3_2_1_40_1","volume-title":"The library used to manipulate DBMs in UPPAAL. (2020)","author":"Library UPPAAL DBM","unstructured":"UPPAAL DBM Library . 2020. The library used to manipulate DBMs in UPPAAL. (2020) . http:\/\/people.cs.aau.dk\/~adavid\/UDBM\/, Last accessed on 2020-06-18. UPPAAL DBM Library. 2020. The library used to manipulate DBMs in UPPAAL. (2020). http:\/\/people.cs.aau.dk\/~adavid\/UDBM\/, Last accessed on 2020-06-18."},{"key":"e_1_3_2_1_41_1","volume-title":"Patients put at risk by computer viruses. The Wall Street Journal","author":"Weaver Christopher","year":"2013","unstructured":"Christopher Weaver . 2013. Patients put at risk by computer viruses. The Wall Street Journal ( 2013 ). Christopher Weaver. 2013. Patients put at risk by computer viruses. The Wall Street Journal (2013)."}],"event":{"name":"MEMOCODE '21: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design","location":"Virtual Event China","acronym":"MEMOCODE '21","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"]},"container-title":["Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3487212.3487342","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3487212.3487342","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:47Z","timestamp":1750191527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3487212.3487342"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,20]]},"references-count":41,"alternative-id":["10.1145\/3487212.3487342","10.1145\/3487212"],"URL":"https:\/\/doi.org\/10.1145\/3487212.3487342","relation":{},"subject":[],"published":{"date-parts":[[2021,11,20]]},"assertion":[{"value":"2021-12-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}