{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T20:36:25Z","timestamp":1740170185158,"version":"3.37.3"},"reference-count":12,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"5","license":[{"start":{"date-parts":[[2015,10,1]],"date-time":"2015-10-01T00:00:00Z","timestamp":1443657600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2015,10,1]],"date-time":"2015-10-01T00:00:00Z","timestamp":1443657600000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2015,10,1]],"date-time":"2015-10-01T00:00:00Z","timestamp":1443657600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2015,10,1]],"date-time":"2015-10-01T00:00:00Z","timestamp":1443657600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS 10-54247"],"award-info":[{"award-number":["CNS 10-54247"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Security Agencys Science of Security Lablets program","award":["W911NSF-13-0086"],"award-info":[{"award-number":["W911NSF-13-0086"]}]},{"DOI":"10.13039\/100000005","name":"U.S. Department of Defense","doi-asserted-by":"publisher","award":["YIP FA9550-12-1-0336"],"award-info":[{"award-number":["YIP FA9550-12-1-0336"]}],"id":[{"id":"10.13039\/100000005","id-type":"DOI","asserted-by":"publisher"}]},{"name":"ERC PoC VERIPACE","award":["620196"],"award-info":[{"award-number":["620196"]}]},{"name":"ERC AdG VERIWARE","award":["246967"],"award-info":[{"award-number":["246967"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Des. Test"],"published-print":{"date-parts":[[2015,10]]},"DOI":"10.1109\/mdat.2015.2448543","type":"journal-article","created":{"date-parts":[[2015,6,22]],"date-time":"2015-06-22T18:28:06Z","timestamp":1434997686000},"page":"27-34","source":"Crossref","is-referenced-by-count":2,"title":["Simulation-Based Verification of Cardiac Pacemakers With Guaranteed Coverage"],"prefix":"10.1109","volume":"32","author":[{"given":"Zhenqi","family":"Huang","sequence":"first","affiliation":[]},{"given":"Chuchu","family":"Fan","sequence":"additional","affiliation":[]},{"given":"Alexandru","family":"Mereacre","sequence":"additional","affiliation":[]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref4","first-page":"131","article-title":"A Simulink hybrid heart model for quantitative verification of cardiac pacemakers","author":"chen","year":"0","journal-title":"Proc 16th Int Conf Hybrid Syst Comput Control"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-642-28756-5_14","article-title":"Modeling and verification of a dual chamber implantable pacemaker","author":"jiang","year":"2012","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658604"},{"key":"ref11","first-page":"216","article-title":"Efficient modeling of excitable cells using hybrid automata","volume":"5","author":"ye","year":"0","journal-title":"Proc Conf Comput Methods Syst Biol"},{"key":"ref5","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/978-3-642-22110-1_31","article-title":"From cardiac cells to genetic regulatory networks","author":"grosu","year":"2011","journal-title":"Computer Aided Verification"},{"journal-title":"“The C2E2 user's guide","year":"2014","author":"duggirala","key":"ref12"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562126"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_25"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","article-title":"Statistical model checking: An overview","author":"legay","year":"2010","journal-title":"Runtime Verification"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71493-4_16"},{"journal-title":"S-Taliro A Tool for Temporal Logic Falsification for Hybrid Systems","year":"2011","author":"annpureddy","key":"ref1"}],"container-title":["IEEE Design & Test"],"original-title":[],"link":[{"URL":"http:\/\/ieeexplore.ieee.org\/ielaam\/6221038\/7236939\/7130608-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6221038\/7236939\/07130608.pdf?arnumber=7130608","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,8]],"date-time":"2022-04-08T18:53:20Z","timestamp":1649444000000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7130608\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10]]},"references-count":12,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.1109\/mdat.2015.2448543","relation":{},"ISSN":["2168-2356","2168-2364"],"issn-type":[{"type":"print","value":"2168-2356"},{"type":"electronic","value":"2168-2364"}],"subject":[],"published":{"date-parts":[[2015,10]]}}}