{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T17:19:38Z","timestamp":1779124778879,"version":"3.51.4"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T00:00:00Z","timestamp":1506470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002341","name":"Academy of Finland","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","award":["2015-04154"],"award-info":[{"award-number":["2015-04154"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]},{"name":"University of Auckland Faculty Research Development Fund","award":["3707500"],"award-info":[{"award-number":["3707500"]}]},{"DOI":"10.13039\/100000001","name":"U.S. National Science Foundation","doi-asserted-by":"publisher","award":["#1329759 and #1139138"],"award-info":[{"award-number":["#1329759 and #1139138"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["PRETSY2 and DFG HA 4407\/6-2"],"award-info":[{"award-number":["PRETSY2 and DFG HA 4407\/6-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2017,10,31]]},"abstract":"<jats:p>Many implantable medical devices, such as pacemakers, have been recalled due to failure of their embedded software. This motivates rethinking their design and certification processes. We propose, for the first time, an additional layer of safety by formalising the problem of run-time enforcement of implantable pacemakers. While recent work has formalised run-time enforcement of reactive systems, the proposed framework generalises existing work along the following directions: (1) we develop bi-directional enforcement, where the enforced policies depend not only on the status of the pacemaker (the controller) but also of the heart (the plant), thus formalising the run-time enforcement problem for cyber-physical systems (2) we express policies using a variant of discrete timed automata (DTA), which can cover all regular properties unlike earlier frameworks limited to safety properties, (3) we are able to ensure the timing safety of implantable devices through the proposed enforcement, and (4) we show that the DTA-based approach is efficient relative to its dense time variant while ensuring that the discretisation error is relatively small and bounded. The developed approach is validated through a prototype system implemented using the open source KIELER framework. The experiments show that the framework incurs minimal runtime overhead.<\/jats:p>","DOI":"10.1145\/3126500","type":"journal-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T12:33:53Z","timestamp":1506515633000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":47,"title":["Runtime Enforcement of Cyber-Physical Systems"],"prefix":"10.1145","volume":"16","author":[{"given":"Srinivas","family":"Pinisetty","sequence":"first","affiliation":[{"name":"Aalto University, Finland and University of Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Partha S.","family":"Roop","sequence":"additional","affiliation":[{"name":"University of Auckland, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"Smyth","sequence":"additional","affiliation":[{"name":"Kiel University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nathan","family":"Allen","sequence":"additional","affiliation":[{"name":"University of Auckland, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[{"name":"Aalto University, Finland and UC Berkeley, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reinhard Von","family":"Hanxleden","sequence":"additional","affiliation":[{"name":"Kiel University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2971808.2972003"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2013.49"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings. 2001 International Conference on. IEEE, 133--142","author":"Andre Charles","year":"2001","unstructured":"Charles Andre , Fr\u00e9d\u00e9ric Boulanger , and Alain Girault . 2001 . Software implementation of synchronous programs. In Application of Concurrency to System Design, 2001 . Proceedings. 2001 International Conference on. IEEE, 133--142 . Charles Andre, Fr\u00e9d\u00e9ric Boulanger, and Alain Girault. 2001. Software implementation of synchronous programs. In Application of Concurrency to System Design, 2001. Proceedings. 2001 International Conference on. IEEE, 133--142."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646704.701880"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000367.2000368"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461351"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-014-0239-8"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.02.008"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0114-4"},{"key":"e_1_2_1_13_1","volume-title":"Algebraic Methodology and Software Technology (AMAST\u201993)","author":"Halbwachs Nicolas","unstructured":"Nicolas Halbwachs , Fabienne Lagnier , and Pascal Raymond . 1994. Synchronous observers and the verification of reactive systems . In Algebraic Methodology and Software Technology (AMAST\u201993) . Springer , 83--96. Nicolas Halbwachs, Fabienne Lagnier, and Pascal Raymond. 1994. Synchronous observers and the verification of reactive systems. In Algebraic Methodology and Software Technology (AMAST\u201993). Springer, 83--96."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-013-0289-7"},{"key":"e_1_2_1_15_1","first-page":"1","article-title":"Cyber-physical modeling of implantable cardiac medical devices","volume":"100","author":"Jiang Z.","year":"2012","unstructured":"Z. Jiang , M. Pajic , and R. Mangharam . 2012 . Cyber-physical modeling of implantable cardiac medical devices . Proc. IEEE 100 , 1 (Jan 2012), 122--137. Z. Jiang, M. Pajic, and R. Mangharam. 2012. Cyber-physical modeling of implantable cardiac medical devices. Proc. IEEE 100, 1 (Jan 2012), 122--137.","journal-title":"Proc. IEEE"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_14"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICHI.2014.11"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455526.1455532"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0215-y"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/353323.353382"},{"key":"e_1_2_1_21_1","volume-title":"Avinash Malik, and Mark Trew.","author":"Partha","year":"2016","unstructured":"Partha S. Roop Sidharta Andalam , Avinash Malik, and Mark Trew. 2016 . Hybrid automata model of the heart for formal verification of pacemakers. In Applied Verification for Continuous and Hybrid Systems (ARCH\u201916). Vienna, Austria . Partha S. Roop Sidharta Andalam, Avinash Malik, and Mark Trew. 2016. Hybrid automata model of the heart for formal verification of pacemakers. In Applied Verification for Continuous and Hybrid Systems (ARCH\u201916). Vienna, Austria."},{"key":"e_1_2_1_22_1","volume-title":"Program Repair without Regret","author":"von Essen Christian","unstructured":"Christian von Essen and Barbara Jobstmann . 2013. Program Repair without Regret . Springer , Berlin, Heidelberg , 896--911. Christian von Essen and Barbara Jobstmann. 2013. Program Repair without Regret. Springer, Berlin, Heidelberg, 896--911."},{"key":"e_1_2_1_23_1","volume-title":"2011 Proceedings IEEE INFOCOM. 1862--1870","author":"Xu F.","unstructured":"F. Xu , Z. Qin , C. C. Tan , B. Wang , and Q. Li . 2011. IMDGuard: Securing implantable medical devices with the external wearable guardian . In 2011 Proceedings IEEE INFOCOM. 1862--1870 . F. Xu, Z. Qin, C. C. Tan, B. Wang, and Q. Li. 2011. IMDGuard: Securing implantable medical devices with the external wearable guardian. In 2011 Proceedings IEEE INFOCOM. 1862--1870."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1049\/iet-syb:20070001"},{"key":"e_1_2_1_25_1","volume-title":"Towards the emulation of the cardiac conduction system for pacemaker testing. arXiv Preprint arXiv:1603.05315","author":"Yip Eugene","year":"2016","unstructured":"Eugene Yip , Sidharta Andalam , Partha S. Roop , Avinash Malik , Mark Trew , Weiwei Ai , and Nitish Patel . 2016. Towards the emulation of the cardiac conduction system for pacemaker testing. arXiv Preprint arXiv:1603.05315 ( 2016 ). Eugene Yip, Sidharta Andalam, Partha S. Roop, Avinash Malik, Mark Trew, Weiwei Ai, and Nitish Patel. 2016. Towards the emulation of the cardiac conduction system for pacemaker testing. arXiv Preprint arXiv:1603.05315 (2016)."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126500","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3126500","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3126500","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:01Z","timestamp":1750273501000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126500"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,27]]},"references-count":25,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.1145\/3126500"],"URL":"https:\/\/doi.org\/10.1145\/3126500","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,27]]},"assertion":[{"value":"2017-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}