{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T22:04:34Z","timestamp":1767650674438,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,4,8]],"date-time":"2013-04-08T00:00:00Z","timestamp":1365379200000},"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":[[2013,4,8]]},"DOI":"10.1145\/2461328.2461351","type":"proceedings-article","created":{"date-parts":[[2013,4,9]],"date-time":"2013-04-09T12:19:32Z","timestamp":1365509972000},"page":"131-136","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["A simulink hybrid heart model for quantitative verification of cardiac pacemakers"],"prefix":"10.1145","author":[{"given":"Taolue","family":"Chen","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Diciolla","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandru","family":"Mereacre","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,4,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.77"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1088\/0967-3334\/31\/5\/001"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_44"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2010.36"},{"issue":"1","key":"e_1_3_2_1_5_1","first-page":"122","volume":"100","author":"Jiang Z.","year":"2012","unstructured":"Z. Jiang , M. Pajic , and R. Mangharam . Cyber-Physical Modeling of Implantable Cardiac Medical Devices. Proceedings of the IEEE , 100 ( 1 ): 122 -- 137 , 2012 . Z. Jiang, M. Pajic, and R. Mangharam. Cyber-Physical Modeling of Implantable Cardiac Medical Devices. Proceedings of the IEEE, 100(1):122--137, 2012.","journal-title":"Cyber-Physical Modeling of Implantable Cardiac Medical Devices. Proceedings of the IEEE"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_14"},{"key":"e_1_3_2_1_7_1","first-page":"585","volume-title":"PRISM 4.0: Verification of Probabilistic Real-time Systems CAV'11","author":"Kwiatkowska M.","year":"2011","unstructured":"M. Kwiatkowska , G. Norman and D. Parker . PRISM 4.0: Verification of Probabilistic Real-time Systems CAV'11 , pp. 585 -- 591 , 2011 . M. Kwiatkowska, G. Norman and D. Parker.PRISM 4.0: Verification of Probabilistic Real-time Systems CAV'11, pp. 585--591, 2011."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038667"},{"key":"e_1_3_2_1_9_1","volume-title":"UPPAAL in a Nutshell","author":"Larsen K. G.","year":"1997","unstructured":"K. G. Larsen , P. Pettersson , and W. Yi . UPPAAL in a Nutshell , 1997 . K. G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a Nutshell, 1997."},{"key":"e_1_3_2_1_10_1","volume-title":"Probabilistic Verification and Approximation. Ann. Pure Appl. Logic, 152(1--3):122--131","author":"Lassaigne R.","year":"2008","unstructured":"R. Lassaigne and S. Peyronnet . Probabilistic Verification and Approximation. Ann. Pure Appl. Logic, 152(1--3):122--131 , 2008 . R. Lassaigne and S. Peyronnet. Probabilistic Verification and Approximation. Ann. Pure Appl. Logic, 152(1--3):122--131, 2008."},{"key":"e_1_3_2_1_11_1","first-page":"122","volume-title":"LNCS 6418","author":"Legay A.","year":"2010","unstructured":"A. Legay , B. Delahaye , and S. Bensalem . Statistical Model Checking: An Overview. RV'10 , LNCS 6418 , pp. 122 -- 135 . Springer , 2010 . A. Legay, B. Delahaye, and S. Bensalem. Statistical Model Checking: An Overview. RV'10, LNCS 6418, pp. 122--135. Springer, 2010."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SSIRI.2010.28"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_14"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0038-092X(93)90060-2"},{"issue":"3","key":"e_1_3_2_1_15_1","first-page":"289","article-title":"A Dynamical Model for Generating Synthetic Electrocardiogram Signals. Biomedical Engineering","volume":"50","author":"McSharry P.","year":"2003","unstructured":"P. McSharry , G. Clifford , L. Tarassenko , and L. Smith . A Dynamical Model for Generating Synthetic Electrocardiogram Signals. Biomedical Engineering , IEEE Transactions on , 50 ( 3 ): 289 -- 294 , 2003 . P. McSharry, G. Clifford, L. Tarassenko, and L. Smith. A Dynamical Model for Generating Synthetic Electrocardiogram Signals. Biomedical Engineering, IEEE Transactions on, 50(3):289 --294, 2003.","journal-title":"IEEE Transactions on"},{"key":"e_1_3_2_1_16_1","volume-title":"Pacemaker's Functional Behaviors in Event-B. Rapport de recherche","author":"M\u00e9ry D.","year":"2009","unstructured":"D. M\u00e9ry and N. K. Singh . Pacemaker's Functional Behaviors in Event-B. Rapport de recherche , 2009 . D. M\u00e9ry and N. K. Singh. Pacemaker's Functional Behaviors in Event-B. Rapport de recherche, 2009."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33636-2_19"},{"key":"e_1_3_2_1_18_1","volume-title":"CMSB","author":"Ye P.","year":"2005","unstructured":"P. Ye , E. Entcheva , R. Grosu , and S. A. Smolka . Efficient Modeling of Excitable Cells Using Hybrid Automata . CMSB , 2005 . P. Ye, E. Entcheva, R. Grosu, and S. A. Smolka. Efficient Modeling of Excitable Cells Using Hybrid Automata. CMSB, 2005."}],"event":{"name":"HSCC '13: Computation and Control","sponsor":["IEEE Signal Processing Society","SIGBED ACM Special Interest Group on Embedded Systems"],"location":"Philadelphia Pennsylvania USA","acronym":"HSCC '13"},"container-title":["Proceedings of the 16th international conference on Hybrid systems: computation and control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2461328.2461351","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2461328.2461351","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:43Z","timestamp":1750234723000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2461328.2461351"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,8]]},"references-count":18,"alternative-id":["10.1145\/2461328.2461351","10.1145\/2461328"],"URL":"https:\/\/doi.org\/10.1145\/2461328.2461351","relation":{},"subject":[],"published":{"date-parts":[[2013,4,8]]},"assertion":[{"value":"2013-04-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}