{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:43:02Z","timestamp":1779392582649,"version":"3.53.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642287558","type":"print"},{"value":"9783642287565","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_14","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:57:15Z","timestamp":1332449835000},"page":"188-203","source":"Crossref","is-referenced-by-count":77,"title":["Modeling and Verification of a Dual Chamber Implantable Pacemaker"],"prefix":"10.1007","author":[{"given":"Zhihao","family":"Jiang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Miroslav","family":"Pajic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Salar","family":"Moarref","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rahul","family":"Mangharam","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"List of Device Recalls, U.S. Food and Drug Admin. (last visited July 19, 2010)"},{"key":"14_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":"14_CR3","unstructured":"AUTOSAR website: \n                    \n                      http:\/\/www.autosar.org\/"},{"key":"14_CR4","unstructured":"AVSI website: \n                    \n                      http:\/\/www.avsi.aero"},{"key":"14_CR5","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/s10009-003-0132-7","volume":"5","author":"R. Alur","year":"2004","unstructured":"Alur, R., Arney, D., Gunter, E.L., Lee, I., Lee, J., Nam, W., Pearce, F., Van Albert, S., Zhou, J.: Formal Specifications and Analysis of the Computer-Assisted Resuscitation Algorithm (CARA) Infusion Pump Control System. Intl. Journal on Software Tools for Technology Transfer (STTT)\u00a05, 308\u2013319 (2004)","journal-title":"Intl. Journal on Software Tools for Technology Transfer (STTT)"},{"issue":"3","key":"14_CR6","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/j.artmed.2005.10.006","volume":"36","author":"A. Teije ten","year":"2006","unstructured":"ten Teije, A., et al.: Improving medical protocols by formal methods. Artificial Intelligence in Medicine\u00a036(3), 193\u2013209 (2006)","journal-title":"Artificial Intelligence in Medicine"},{"key":"14_CR7","unstructured":"PACEMAKER System Specification. Boston Scientific (2007)"},{"key":"14_CR8","unstructured":"The Compass - Technical Guide to Boston Scientific Cardiac Rhythm Management Products (2007)"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer (STTT), 134\u2013152 (1997)","DOI":"10.1007\/s100090050010"},{"key":"14_CR10","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Pacemaker UPPAAL model download: \n                    \n                      http:\/\/www.seas.upenn.edu\/~zhihaoj\/VHM\/PM_verify.zip"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Pajic, M., Jiang, Z., Sokolsky, O., Lee, I., Mangharam, R.: From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study. In: 18th IEEE Real-Time and Embedded Technology and Applications Symposium, IEEE RTAS (2012)","DOI":"10.1109\/RTAS.2012.25"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Barold, S., Stroobandt, R., Sinnaeve, A.: Cardiac Pacemakers Step by Step. Blackwell Futura (2004)","DOI":"10.1002\/9780470750728"},{"key":"14_CR13","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Allen Emerson, E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, pp. 52\u201371 (1982)","DOI":"10.1007\/BFb0025774"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Jiang, Z., Pajic, M., Mangharam, R.: Model-based Closed-loop Testing of Implantable Pacemakers. In: ICCPS 2011: ACM\/IEEE 2nd Intl. Conf. on Cyber-Physical Systems (2011)","DOI":"10.1109\/ICCPS.2011.28"},{"key":"14_CR17","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":"14_CR18","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. In: Fourth International Conference on Secure Software Integration and Reliability Improvement, pp. 23\u201332 (2010)","DOI":"10.1109\/SSIRI.2010.28"},{"key":"14_CR19","unstructured":"Wiggelinkhuizen, J.E.: Feasibility of Formal Model Checking in the Vitatron Environment. Master thesis, Eindhoven University of Technology (2007)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-68237-0_14","volume-title":"FM 2008: Formal Methods","author":"H.D. Macedo","year":"2008","unstructured":"Macedo, H.D., Larsen, P.G., Fitzgerald, J.S.: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 181\u2013197. Springer, Heidelberg (2008)"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-642-05089-3_44","volume-title":"FM 2009: Formal Methods","author":"A.O. Gomes","year":"2009","unstructured":"Gomes, A.O., Oliveira, M.V.M.: Formal Specification of a Cardiac Pacing System. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 692\u2013707. Springer, Heidelberg (2009)"},{"key":"14_CR22","unstructured":"Mery, D., Singh, N.K.: Pacemaker\u2019s Functional Behaviors in Event-B. Research report, INRIA (2009)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:08:47Z","timestamp":1620126527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}