{"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":1774801916487,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,9,24]],"date-time":"2013-09-24T00:00:00Z","timestamp":1379980800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10009-013-0289-7","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T15:55:22Z","timestamp":1379951722000},"page":"191-213","source":"Crossref","is-referenced-by-count":38,"title":["Closed-loop verification of medical devices with model abstraction and refinement"],"prefix":"10.1007","volume":"16","author":[{"given":"Zhihao","family":"Jiang","sequence":"first","affiliation":[]},{"given":"Miroslav","family":"Pajic","sequence":"additional","affiliation":[]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[]},{"given":"Rahul","family":"Mangharam","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,9,24]]},"reference":[{"key":"289_CR1","unstructured":"List of Device Recalls, U.S. Food and Drug Admin., (last visited Jul. 19, 2010)"},{"key":"289_CR2","unstructured":"Sandler, K., Ohrstrom, L., Moy, L., McVay R.: Killed by Code: Software Transparency in Implantable Medical Devices. Software Freedom Law Center (2010)"},{"key":"289_CR3","unstructured":"AUTOSAR. http:\/\/www.autosar.org\/"},{"key":"289_CR4","unstructured":"AVSI. http:\/\/www.avsi.aero"},{"key":"289_CR5","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"289_CR6","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. (STTT) 134\u2013152 (1997)","DOI":"10.1007\/s100090050010"},{"key":"289_CR7","volume-title":"Clinical Cardiac Electrophysiology","author":"ME Josephson","year":"2008","unstructured":"Josephson, M.E.: Clinical Cardiac Electrophysiology. Lippincot Williams and Wilkins, Baltimore (2008)"},{"key":"289_CR8","doi-asserted-by":"crossref","DOI":"10.1002\/9780470750728","volume-title":"Cardiac Pacemakers Step by Step","author":"S Barold","year":"2004","unstructured":"Barold, S., Stroobandt, R., Sinnaeve, A.: Cardiac Pacemakers Step by Step. Blackwell Futura, Hoboken (2004)"},{"issue":"5","key":"289_CR9","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"289_CR10","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking (2000)"},{"issue":"5","key":"289_CR11","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Helmut, V.: Counter example-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"289_CR12","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-642-28756-5_14","volume":"7214","author":"Z Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. Tools Algorith. Construct. Anal. Syst. 7214, 188\u2013203 (2012)","journal-title":"Tools Algorith. Construct. Anal. Syst."},{"key":"289_CR13","unstructured":"The Compass\u2013Technical Guide to Boston Scientific Cardiac Rhythm Management Products (2007)"},{"key":"289_CR14","unstructured":"Jiang, Z., Pajic, M., Alur, A., Rahul, M.: Pacemaker UPPAAL model download: http:\/\/mlab.seas.upenn.edu"},{"key":"289_CR15","doi-asserted-by":"crossref","unstructured":"Pajic, M., Jiang, Z., Lee, I., Sokolsky, O., Rahul, M.: From verification to implementation: a model translation tool and a pacemaker case study. In: Proceedings of the 2012 IEEE 18th Real Time and Embedded Technology and Applications Symposium, RTAS \u201912, pp. 173\u2013184 (2012)","DOI":"10.1109\/RTAS.2012.25"},{"key":"289_CR16","volume-title":"EP testing","author":"RN Fogoros","year":"1999","unstructured":"Fogoros, R.N.: EP testing. Blackwell Science, New York (1999)"},{"key":"289_CR17","doi-asserted-by":"crossref","unstructured":"Yamane, S.: Timed weak simulation verification and its application to stepwise refinement of real time software. Int. J. Comput. Sci. Netw. Secur. 6 (2006)","DOI":"10.1007\/11596356_40"},{"key":"289_CR18","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL, pp. 200\u2013236. Formal Methods for the Design of Real-Time Systems. Lecture Notes in Computer Science (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"289_CR19","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, pp. 52\u201371 (1982)","DOI":"10.1007\/BFb0025774"},{"issue":"1","key":"289_CR20","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1109\/JPROC.2011.2161241","volume":"100","author":"Z Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Mangharam, R.: Cyber-Physical modeling of implantable cardiac medical devices. Proc. IEEE 100(1), 122\u2013137 (2012)","journal-title":"Proc. IEEE"},{"key":"289_CR21","doi-asserted-by":"crossref","unstructured":"Jiang, Z., Mangharam, R.: Modeling cardiac pacemaker malfunctions with the virtual heart model. In: Engineering in Medicine and Biology Society, EMBC, 2011 Annual International Conference of the IEEE, pp. 263\u2013266 (2011)","DOI":"10.1109\/IEMBS.2011.6090051"},{"key":"289_CR22","doi-asserted-by":"crossref","unstructured":"Jiang, Z., Pajic, M., Mangharam, R.: Model-based closed-loop testing of implantable pacemakers. In: ICCPS\u201911: ACM\/IEEE 2nd Intl. Conf. on Cyber-Physical Systems (2011)","DOI":"10.1109\/ICCPS.2011.28"},{"key":"289_CR23","unstructured":"PACEMAKER System Specification. Boston Scientific, Natick (2007)"},{"key":"289_CR24","unstructured":"Jiang, Z., Radhakrishnan, S., Sampath, V., Sarode, S., Pajic, M., Mangharam, R.: Heart-on-a-Chip: a closed-loop testing platform for implantable pacemakers. In: Third Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy), CPS Week (2013)"},{"key":"289_CR25","doi-asserted-by":"crossref","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers. In: Hybrid Systems: Computation and Control (HSCC 2013) (2013)","DOI":"10.1145\/2461328.2461351"},{"key":"289_CR26","doi-asserted-by":"crossref","unstructured":"Jee, E., Wang, S., Kim, J. K., Lee, J., Sokolsky, O., Lee, I.: A safety-assured development approach for real-time software. In: The Proceedings of 16th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, pp. 133\u2013142 (2010)","DOI":"10.1109\/RTCSA.2010.42"},{"key":"289_CR27","doi-asserted-by":"crossref","unstructured":"Tuan, L.A., Zheng, M.C., Tho, Q.T.: Modeling and verification of safety critical systems: a case study on pacemaker. Fourth International Conference on Secure Software Integration and Reliability Improvement, pp. 23\u201332 (2010)","DOI":"10.1109\/SSIRI.2010.28"},{"key":"289_CR28","unstructured":"Wiggelinkhuizen, J.E.: Feasibility of Formal Model Checking in the Vitatron Environment. Eindhoven University of Technology, Master thesis (2007)"},{"key":"289_CR29","unstructured":"Macedo, H.D., Larsen, P.G., Fitzgerald, J.: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System using VDM, pp. 28\u201330. Formal Methods (2008)"},{"key":"289_CR30","doi-asserted-by":"crossref","unstructured":"Gomes, A.O., Oliveira, M.V.: Formal specification of a cardiac pacing system. In: Proceedings of the 2nd World Congress on Formal Methods (FM \u201909), pp. 692\u2013707 (2009)","DOI":"10.1007\/978-3-642-05089-3_44"},{"key":"289_CR31","volume-title":"Pacemaker\u2019s Functional Behaviors in Event-B","author":"D Mery","year":"2009","unstructured":"Mery, D., Singh, N.K.: Pacemaker\u2019s Functional Behaviors in Event-B. Research report, INRIA (2009)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0289-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0289-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0289-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,6]],"date-time":"2022-03-06T17:51:23Z","timestamp":1646589083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0289-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,24]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["289"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0289-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,24]]}}}