{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T16:31:56Z","timestamp":1774801916779,"version":"3.50.1"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4s","license":[{"start":{"date-parts":[[2014,4,1]],"date-time":"2014-04-01T00:00:00Z","timestamp":1396310400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:p>Software-based control of life-critical embedded systems has become increasingly complex, and to a large extent has come to determine the safety of the human being. For example, implantable cardiac pacemakers have over 80,000 lines of code which are responsible for maintaining the heart within safe operating limits. As firmware-related recalls accounted for over 41% of the 600,000 devices recalled in the last decade, there is a need for rigorous model-driven design tools to generate verified code from verified software models. To this effect, we have developed the UPP2SF model-translation tool, which facilitates automatic conversion of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink\/Stateflow). We describe the translation rules that ensure correct model conversion, applicable to a large class of models. We demonstrate how UPP2SF is used in the model-driven design of a pacemaker whose model is (a) designed and verified in UPPAAL (using timed automata), (b) automatically translated to Stateflow for simulation-based testing, and then (c) automatically generated into modular code for hardware-level integration testing of timing-related errors. In addition, we show how UPP2SF may be used for worst-case execution time estimation early in the design stage. Using UPP2SF, we demonstrate the value of integrated end-to-end modeling, verification, code-generation and testing process for complex software-controlled embedded systems.<\/jats:p>","DOI":"10.1145\/2584651","type":"journal-article","created":{"date-parts":[[2014,4,8]],"date-time":"2014-04-08T12:24:20Z","timestamp":1396959860000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Safety-critical medical device development using the UPP2SF model translation tool"],"prefix":"10.1145","volume":"13","author":[{"given":"Miroslav","family":"Pajic","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhihao","family":"Jiang","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rahul","family":"Mangharam","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,4]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11603009_21"},{"key":"e_1_2_2_2_1","first-page":"688","article-title":"Timed automata","volume":"1633","author":"Alur R.","year":"1999","unstructured":"R. Alur . 1999 . Timed automata . In Computer Aided Verification , 1633 , 688 -- 688 . R. Alur. 1999. Timed automata. In Computer Aided Verification, 1633, 688--688.","journal-title":"Computer Aided Verification"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40903-8_6"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11811-1_37"},{"key":"e_1_2_2_6_1","first-page":"33","article-title":"A tutorial on UPPAAL","volume":"3185","author":"Behrmann G.","year":"2004","unstructured":"G. Behrmann , A. David , and K. Larsen . 2004 . A tutorial on UPPAAL . In Formal Methods for the Design of Real-Time Systems , vol. 3185 , 33 -- 35 . G. Behrmann, A. David, and K. Larsen. 2004. A tutorial on UPPAAL. In Formal Methods for the Design of Real-Time Systems, vol. 3185, 33--35.","journal-title":"Formal Methods for the Design of Real-Time Systems"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"e_1_2_2_8_1","unstructured":"Boston Scientific. 2007. PACEMAKER System Specification. (2007).  Boston Scientific. 2007. PACEMAKER System Specification. (2007)."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/225014.225019"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086260"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0049-7"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2010.36"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2161241"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_14"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038667"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.127"},{"key":"e_1_2_2_20_1","volume-title":"Proceedings of the ERCIM Workshop on Formal Methods for Industrial Critical Systems.","author":"Leitner F.","unstructured":"F. Leitner and S. Leue . 2008. Simulink design verifier vs. SPIN - a comparative case study . In Proceedings of the ERCIM Workshop on Formal Methods for Industrial Critical Systems. F. Leitner and S. Leue. 2008. Simulink design verifier vs. SPIN - a comparative case study. In Proceedings of the ERCIM Workshop on Formal Methods for Industrial Critical Systems."},{"key":"e_1_2_2_21_1","volume-title":"Matlab R2012a Documentation \u2192 Stateflow. http:\/\/www.mathworks.com\/help\/toolbox\/stateflow.","year":"2012","unstructured":"Matlab. 2012 . Matlab R2012a Documentation \u2192 Stateflow. http:\/\/www.mathworks.com\/help\/toolbox\/stateflow. (2012). Matlab. 2012. Matlab R2012a Documentation \u2192 Stateflow. http:\/\/www.mathworks.com\/help\/toolbox\/stateflow. (2012)."},{"key":"e_1_2_2_22_1","unstructured":"Nano-RK. 2013. nano-RK Sensor RTOS. http:\/\/nanork.org.  Nano-RK. 2013. nano-RK Sensor RTOS. http:\/\/nanork.org."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2012.25"},{"key":"e_1_2_2_24_1","volume-title":"Tech. Rep. University of Pennsylvania.","author":"Pajic M.","year":"2012","unstructured":"M. Pajic , I. Lee , R. Mangharam , and O. Sokolsky . 2012 b. UPP2SF: Translating UPPAAL models to Simulink . Tech. Rep. University of Pennsylvania. M. Pajic, I. Lee, R. Mangharam, and O. Sokolsky. 2012b. UPP2SF: Translating UPPAAL models to Simulink. Tech. Rep. University of Pennsylvania."},{"key":"e_1_2_2_25_1","first-page":"13","article-title":"Model-driven safety analysis of closed-loop medical systems","volume":"99","author":"Pajic M.","year":"2012","unstructured":"M. Pajic , R. Mangharam , O. Sokolsky , D. Arney , J. Goldman , and I. Lee . 2012 c. Model-driven safety analysis of closed-loop medical systems . IEEE Trans. Indust. Inf. 99 , 13 . DOI: http:\/\/dx.doi.org\/10. 1109\/TII.2012.2226594 M. Pajic, R. Mangharam, O. Sokolsky, D. Arney, J. Goldman, and I. Lee. 2012c. Model-driven safety analysis of closed-loop medical systems. IEEE Trans. Indust. Inf. 99, 13. DOI: http:\/\/dx.doi.org\/10. 1109\/TII.2012.2226594","journal-title":"IEEE Trans. Indust. Inf."},{"key":"e_1_2_2_26_1","volume-title":"Killed by code: Software transparency in implantable medical devices. Softw. Free","author":"Sandler K.","unstructured":"K. Sandler , L. Ohrstrom , L. Moy , and R. McVay . 2010. Killed by code: Software transparency in implantable medical devices. Softw. Free . Law Center . K. Sandler, L. Ohrstrom, L. Moy, and R. McVay. 2010. Killed by code: Software transparency in implantable medical devices. Softw. Free. Law Center."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017753.1017795"},{"key":"e_1_2_2_28_1","unstructured":"Max Schurenberg. 2012. Scalability analysis of the simulink design verifier on an avionic system. Bachelor thesis TU Hamburg-Harburg.  Max Schurenberg. 2012. Scalability analysis of the simulink design verifier on an avionic system. Bachelor thesis TU Hamburg-Harburg."},{"key":"e_1_2_2_29_1","unstructured":"US FDA. 2010. List of Device Recalls U.S. Food and Drug Admin. (Last accessed 7\/10).  US FDA. 2010. List of Device Recalls U.S. Food and Drug Admin. (Last accessed 7\/10)."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2584651","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2584651","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:01:43Z","timestamp":1750230103000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2584651"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4]]},"references-count":28,"journal-issue":{"issue":"4s","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1145\/2584651"],"URL":"https:\/\/doi.org\/10.1145\/2584651","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4]]},"assertion":[{"value":"2012-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}