{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:34:29Z","timestamp":1759638869388,"version":"3.41.0"},"reference-count":71,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"9","license":[{"start":{"date-parts":[[2018,9,1]],"date-time":"2018-09-01T00:00:00Z","timestamp":1535760000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2018,9,1]],"date-time":"2018-09-01T00:00:00Z","timestamp":1535760000000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2018,9,1]],"date-time":"2018-09-01T00:00:00Z","timestamp":1535760000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2018,9,1]],"date-time":"2018-09-01T00:00:00Z","timestamp":1535760000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. IEEE"],"published-print":{"date-parts":[[2018,9]]},"DOI":"10.1109\/jproc.2018.2853608","type":"journal-article","created":{"date-parts":[[2018,8,7]],"date-time":"2018-08-07T18:55:56Z","timestamp":1533668156000},"page":"1593-1615","source":"Crossref","is-referenced-by-count":10,"title":["Real-Time Decision Policies With Predictable Performance"],"prefix":"10.1109","volume":"106","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-2618","authenticated-orcid":false,"given":"Houssam","family":"Abbas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Konstantinos","family":"Mamouras","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rahul","family":"Mangharam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8455-9917","authenticated-orcid":false,"given":"Alena","family":"Rodionova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref71","first-page":"mt51","article-title":"Enhanced algorithm for glucose estimation using the continuous glucose monitoring system","volume":"16","author":"leal","year":"2010","journal-title":"Med Sci Monitor"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1177\/193229681000400222"},{"key":"ref39","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-46675-9_21","article-title":"Data-oriented characterization of application-level energy optimization","author":"liu","year":"2015","journal-title":"Proc Fundam Approaches Softw Eng"},{"key":"ref38","first-page":"169","article-title":"In-silico pre-clinical trials for implantable cardioverter defibrillators","author":"jiang","year":"2016","journal-title":"Proc IEEE Eng Med Biol Soc Annu Int Conf (EMBC)"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.15"},{"journal-title":"Java’s Lambda Expressions","year":"0","key":"ref32"},{"key":"ref31","doi-asserted-by":"crossref","DOI":"10.1145\/3023147","article-title":"Industrial use of domain-specific modeling: Panel summary","author":"tolvanen","year":"2016","journal-title":"Proceedings of the 10th Workshop on Domain-specific Modeling"},{"key":"ref30","article-title":"Evaluating the use of domain-specific modeling in practice","author":"k\u00e4rn\u00e4","year":"2009","journal-title":"Proc of 6th OOPSLA Workshop on Domain-Specific Modeling"},{"key":"ref37","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1109\/HLDVT.2016.7748260","article-title":"High-level modeling for computer-aided clinical trials of medical devices","author":"abbas","year":"2016","journal-title":"Proc IEEE Int High Level Des Validation Test Workshop (HLDVT)"},{"key":"ref36","first-page":"311","article-title":"Semantics and evaluation techniques for window aggregates in data streams","author":"li","year":"2005","journal-title":"Proc ACM SIGMOD Int Conf Manage Data"},{"key":"ref35","first-page":"15","article-title":"Regular programming for quantitative properties of data streams","author":"alur","year":"2016","journal-title":"Proc 25th Eur Symp Program (ESOP)"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/T-C.1971.223204"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/506147.506151"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1155\/2011\/480805"},{"key":"ref61","doi-asserted-by":"crossref","first-page":"325","DOI":"10.3233\/EMC-2005-00036","article-title":"Integrating functional and power simulation in embedded systems design","volume":"1","author":"ayala","year":"2005","journal-title":"J Embedded Comput"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45716-X_33"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1161\/CIRCOUTCOMES.112.965368"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2007.01.002"},{"key":"ref27","article-title":"A novel strategy to mitigate ICD shock-related pain","author":"berger","year":"2017","journal-title":"Heart Rhythm Scientific Sessions"},{"key":"ref65","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1145\/1013235.1013292","article-title":"Application-level prediction of battery dissipation","author":"krintz","year":"2004","journal-title":"Proc Int Symp Low Power Electron Design"},{"key":"ref66","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/978-3-319-14125-1_5","article-title":"Energy consumption analysis of programs based on XMOS ISA-level models","author":"liqat","year":"2014","journal-title":"Logic-Based Program Synthesis and Transformation"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1093\/europace\/euv436"},{"year":"2017","key":"ref67"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1145\/3046679"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2006.17"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_1"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/2.868693"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.hrthm.2006.05.006"},{"journal-title":"Clinical Cardiac Pacing Defibrillation and Resynchronization Therapy E-Book","year":"2011","author":"ellenbogen","key":"ref22"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1161\/01.CIR.98.7.663"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.hrthm.2017.04.026"},{"journal-title":"BioMonitor Technical Manual","year":"2015","key":"ref23"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67471-1_2"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1111\/pace.13062"},{"key":"ref50","article-title":"STREAM: The Stanford data stream management system","author":"arasu","year":"2004","journal-title":"Stanford Infolab"},{"key":"ref51","first-page":"363","article-title":"Consistent streaming through time: A vision for event stream processing","author":"barga","year":"2007","journal-title":"Proc of the 3rd Biennial Conf on Innovative Data Systems Research (CIDR07)"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2005.26"},{"journal-title":"Apache Flink Scalable Batch and Stream Data Processing","year":"0","key":"ref58"},{"year":"0","key":"ref57"},{"journal-title":"ReactiveX An API for asynchronous programming with observable streams","year":"0","key":"ref56"},{"key":"ref55","first-page":"360","article-title":"Stream processing with a spreadsheet","author":"vaziri","year":"2014","journal-title":"Proc of Euro Conf on Object-Oriented Programming (ECOOP)"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1147\/JRD.2013.2243535"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/s00778-004-0147-z"},{"key":"ref52","first-page":"1242","article-title":"The extensibility framework in Microsoft Streaminsight","author":"ali","year":"2011","journal-title":"Proc IEEE Int Conf on Data Engineering (ICDE)"},{"key":"ref10","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/JPROC.2011.2165270","article-title":"Challenges and research directions in medical cyber-physical systems","volume":"100","author":"lee","year":"2012","journal-title":"Proc IEEE"},{"key":"ref11","first-page":"216","article-title":"Efficient modeling of excitable cells using hybrid automata","author":"ye","year":"2005","journal-title":"Proc Conf Computational Methods in Systems Biology"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-013-0289-7"},{"key":"ref12","first-page":"188","article-title":"Modeling and verification of a dual chamber implantable pacemaker","author":"jiang","year":"2012","journal-title":"Proc Int Conf Tools and Algorithms Constr and Anal Syst"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.01.014"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1002\/spe.1006"},{"journal-title":"The Compass–Technical Guide to Boston Scientific Cardiac Rhythm Management Products","year":"2007","key":"ref17"},{"year":"0","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1371\/journal.pone.0114494"},{"journal-title":"Principles of Cyber-Physical Systems","year":"2015","author":"alur","key":"ref4"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1109\/JPROC.2006.890107","article-title":"Quo vadis, SLD? Reasoning about the trends and challenges of system level design","volume":"95","author":"sangiovanni-vincentelli","year":"2007","journal-title":"Proc IEEE"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"693","DOI":"10.1145\/3062341.3062369","article-title":"StreamQRE: Modular specification and efficient evaluation of quantitative queries over streaming data","author":"mamouras","year":"2017","journal-title":"Proc 38th ACM SIGPLAN Conf Program Lang Des Implement"},{"key":"ref5","first-page":"15","article-title":"Regular programming for quantitative properties of data streams","author":"alur","year":"2016","journal-title":"Proc Eur Symp Programm Lang Syst"},{"journal-title":"NEXMark - a benchmark for queries over data streams","year":"2002","author":"tucker","key":"ref8"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPSW.2016.138"},{"key":"ref49","first-page":"277","article-title":"The design of the Borealis stream processing engine","author":"abadi","year":"2005","journal-title":"Proc 2nd Biennial Conf Innovative Data Systems Research (CIDR 05)"},{"key":"ref9","first-page":"99","article-title":"Quantitative network monitoring with NetQRE","author":"yuan","year":"2017","journal-title":"Proc ACM SIGCOMM Conf Data Commun"},{"key":"ref46","first-page":"7188","article-title":"Hardware-in-the-loop simulation and energy optimization of cardiac pacemakers","author":"barker","year":"2015","journal-title":"Proc IEEE Eng Med Biol Soc Annu Int Conf (EMBC)"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.01.014"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/s00778-003-0095-z"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2015.08.382"},{"key":"ref42","first-page":"23","article-title":"Modeling and verification of safety critical systems: A case study on pacemaker","author":"tuan","year":"2010","journal-title":"Proc 4th Int Conf Secure Softw Integr Rel Improvement"},{"key":"ref41","first-page":"87","article-title":"Towards model checking of implantable cardioverter defibrillators","author":"abbas","year":"2016","journal-title":"Proc 19th Int Conf Hybrid Syst Comput Control"},{"journal-title":"General principles of software validation final guidance for industry and FDA staff","year":"2002","key":"ref44"},{"key":"ref43","first-page":"5595","article-title":"Hybrid automata models of cardiac ventricular electrophysiology for real-time computational applications","author":"andalam","year":"2016","journal-title":"Proc IEEE Eng Med Biol Soc Annu Int Conf (EMBC)"}],"container-title":["Proceedings of the IEEE"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielaam\/5\/8466984\/8428635-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/5\/8466984\/08428635.pdf?arnumber=8428635","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T07:25:56Z","timestamp":1751786756000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8428635\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9]]},"references-count":71,"journal-issue":{"issue":"9"},"URL":"https:\/\/doi.org\/10.1109\/jproc.2018.2853608","relation":{},"ISSN":["0018-9219","1558-2256"],"issn-type":[{"type":"print","value":"0018-9219"},{"type":"electronic","value":"1558-2256"}],"subject":[],"published":{"date-parts":[[2018,9]]}}}