{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:08Z","timestamp":1750220828380,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,9]],"date-time":"2019-10-09T00:00:00Z","timestamp":1570579200000},"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":[],"published-print":{"date-parts":[[2019,10,9]]},"DOI":"10.1145\/3359986.3361200","type":"proceedings-article","created":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T12:21:06Z","timestamp":1570450866000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Securing implantable medical devices with runtime enforcement hardware"],"prefix":"10.1145","author":[{"given":"Hammond","family":"Pearce","sequence":"first","affiliation":[{"name":"University of Auckland, Auckland, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew M. Y.","family":"Kuo","sequence":"additional","affiliation":[{"name":"AUT University, Auckland, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Partha S.","family":"Roop","sequence":"additional","affiliation":[{"name":"University of Auckland, Auckland, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Srinivas","family":"Pinisetty","sequence":"additional","affiliation":[{"name":"I.I.T. Bhubaneswar, Jatni, Odisha, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"K. D. Atherton. 2013. How Dick Cheney Took His Heart Offline To Thwart Hackers. https:\/\/www.popsci.com\/article\/gadgets\/how-dick-cheney-took-his-heart-offline-thwart-hackers"},{"volume-title":"Cardiac Pacemakers step by step: An illustrated guide","author":"Barold S Serge","key":"e_1_3_2_1_2_1","unstructured":"S Serge Barold, Roland X Stroobandt, and Alfons F Sinnaeve. 2008. Cardiac Pacemakers step by step: An illustrated guide. John Wiley & Sons."},{"volume-title":"Towards Certified Runtime Verification","author":"Blech Jan Olaf","key":"e_1_3_2_1_3_1","unstructured":"Jan Olaf Blech, Yli\u00e8s Falcone, and Klaus Becker. 2012. Towards Certified Runtime Verification. In Formal Methods and Software Engineering, Toshiaki Aoki and Kenji Taguchi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 494--509."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.347.6221.499"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043164.2018438"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Cormac Flanagan and Barbara K\u00f6nig (Eds.)","author":"Jiang Zhihao","key":"e_1_3_2_1_7_1","unstructured":"Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, and Rahul Mangharam. 2012. Modeling and Verification of a Dual Chamber Implantable Pacemaker. In Tools and Algorithms for the Construction and Analysis of Systems, Cormac Flanagan and Barbara K\u00f6nig (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 188--203."},{"key":"e_1_3_2_1_8_1","volume-title":"Pacemaker hack can deliver deadly 830-volt jolt. Computerworld 17 (October","author":"Kirk J","year":"2012","unstructured":"J Kirk. 2012. Pacemaker hack can deliver deadly 830-volt jolt. Computerworld 17 (October 2012)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.884574"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/HEALTH.2011.6026732"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0046-8"},{"volume-title":"A Theory of Runtime Enforcement, with Results","author":"Ligatti Jay","key":"e_1_3_2_1_12_1","unstructured":"Jay Ligatti and Srikar Reddy. 2010. A Theory of Runtime Enforcement, with Results.. In ESORICS. Springer, 87--100."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2991079.2991094"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSECP.2004.1281254"},{"key":"e_1_3_2_1_15_1","unstructured":"Medtronic. 2017. Adapta DR pacing system UC200601057c. https:\/\/europe.medtronic.com\/content\/dam\/medtronic-com\/01_crhf\/brady\/pdfs\/200601057cENp6_adapta_dr_pacing_system_spec%20Sheet.pdf"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556922"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126500"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1080\/17434440.2018.1483235"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653712"},{"key":"e_1_3_2_1_20_1","volume-title":"Wall Street Journal (October","author":"Rockoff J. D.","year":"2016","unstructured":"J. D. Rockoff. 2016. J&J Warns Insulin Pump Vulnerable to Cyber Hacking. Wall Street Journal (October 2016)."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516658"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2667218"},{"key":"e_1_3_2_1_23_1","volume-title":"Workshop on Intrusion Detection and Network Monitoring","volume":"1999","author":"Sekar R","year":"1999","unstructured":"R Sekar, Thomas F Bowen, and Mark E Segal. 1999. On Preventing Intrusions by Process Behavior Monitoring.. In Workshop on Intrusion Detection and Network Monitoring, Vol. 1999. 29--40."},{"key":"e_1_3_2_1_24_1","volume-title":"RV-CuBES","volume":"3","author":"Signoles Julien","year":"2017","unstructured":"Julien Signoles, Nikolai Kosmatov, and Kostyantyn Vorobyov. 2017. E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper). In RV-CuBES, Vol. 3. Kalpa Publications in Computing, 164--173."},{"key":"e_1_3_2_1_25_1","volume-title":"Insulin pump hacker says vendor Medtronic is ignoring security risk. Venturebeat (August","author":"Takahashi D","year":"2011","unstructured":"D Takahashi. 2011. Insulin pump hacker says vendor Medtronic is ignoring security risk. Venturebeat (August 2011). https:\/\/venturebeat.com\/2011\/08\/25\/insulin-pump-hacker-says-vendor-medtronic-is-ignoring-security-risk\/"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2010.7"},{"key":"e_1_3_2_1_27_1","unstructured":"University of Oxford. 2019. EBMC. http:\/\/www.cprover.org\/ebmc"},{"key":"e_1_3_2_1_29_1","volume-title":"Patients Put at Risk By Computer Viruses. Wall Street Journal (June","author":"Weaver C","year":"2013","unstructured":"C Weaver. 2013. Patients Put at Risk By Computer Viruses. Wall Street Journal (June 2013)."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2011.5934987"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TBCAS.2013.2245664"}],"event":{"name":"MEMOCODE '19: 17th ACM-IEEE International Conference on Formal Methods and Models for System Design","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"],"location":"La Jolla California","acronym":"MEMOCODE '19"},"container-title":["Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359986.3361200","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3359986.3361200","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:27Z","timestamp":1750202007000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359986.3361200"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,9]]},"references-count":30,"alternative-id":["10.1145\/3359986.3361200","10.1145\/3359986"],"URL":"https:\/\/doi.org\/10.1145\/3359986.3361200","relation":{},"subject":[],"published":{"date-parts":[[2019,10,9]]},"assertion":[{"value":"2019-10-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}