{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T15:31:08Z","timestamp":1729611068528,"version":"3.28.0"},"reference-count":42,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/real.2003.1253272","type":"proceedings-article","created":{"date-parts":[[2004,5,25]],"date-time":"2004-05-25T20:11:16Z","timestamp":1085515876000},"page":"256-264","source":"Crossref","is-referenced-by-count":1,"title":["Generating formal models for real-time verification by exact low-level runtime analysis of synchronous programs"],"prefix":"10.1109","author":[{"given":"G.","family":"Logothetis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.","family":"Schneider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Metzler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2003.1210100"},{"key":"ref38","first-page":"445","article-title":"Introducing mutual ex clusion in Esterel","volume":"1755","author":"schneider","year":"1999","journal-title":"Andrei Ershov Third International Conference Perspectives of Systems Informatics"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2000.845982"},{"key":"ref32","first-page":"76","article-title":"Modeling VHDL in multiclock ESTEREL","author":"rajan","year":"2000","journal-title":"International Conference on VLSI Design"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/BF00571421"},{"key":"ref30","first-page":"16","article-title":"Worst-case execution time analysis at low cost","author":"puschner","year":"1997","journal-title":"Distributed Computer Control Systems"},{"key":"ref37","article-title":"Verification of Reactive Systems - Algorithms and Formal Methods","author":"schneider","year":"2003","journal-title":"EATCS Texts"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_21"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/CSD.2001.981772"},{"key":"ref34","first-page":"205","article-title":"A verified hardware synthesis for Esterel","author":"schneider","year":"2000","journal-title":"Workshop on Distributed and Par allel Embedded Systems (DIPES)"},{"key":"ref10","doi-asserted-by":"crossref","first-page":"1298","DOI":"10.1007\/BFb0002886","article-title":"Deriving annotations for tight calculation of execution time","volume":"1300","author":"ermedahl","year":"1997","journal-title":"European Conference on Parallel Processing (EUROPAR)"},{"key":"ref40","article-title":"Realizing real-time systems from synchronous language specifications","author":"shyamasundar","year":"2000","journal-title":"Real-Time Systems Symposium"},{"journal-title":"Website","article-title":"Esterel Technology","year":"0","key":"ref11"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/325478.325479"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235322"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1992.242675"},{"key":"ref16","article-title":"A general approach for the tight timing predictions of non-rectangular loops","author":"healy","year":"1999","journal-title":"Real-Time Technology and Applications Symposium"},{"journal-title":"S homepage Website","year":"0","key":"ref17"},{"year":"0","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7352"},{"key":"ref28","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0057776","article-title":"Integrating path and timing analysis using instruction-level simulation techniques","author":"lundqvist","year":"1998","journal-title":"Languages Compilers and Tools for Embedded Systems (LCTES)"},{"key":"ref4","article-title":"The foundations of Esterel","author":"berry","year":"1998","journal-title":"Proof Language and Interaction Essays in Honour of Robin Milner"},{"key":"ref27","article-title":"Run time analysis of synchronous programs for low-level real-time verification","author":"logothetis","year":"2003","journal-title":"Symposium on Integrated Cir cuits and System Design (SBCCI)"},{"article-title":"The VHDL cookperiodical","year":"1990","author":"ashenden","key":"ref3"},{"article-title":"The Esterel v5_91 language primer","year":"2000","author":"berry","key":"ref6"},{"article-title":"Predicting instruction cache behavior","year":"1993","author":"mueller","key":"ref29"},{"article-title":"The constructive semantics of pure Esterel","year":"1999","author":"berry","key":"ref5"},{"key":"ref8","article-title":"SugarCubes implementation of causality","author":"boussinot","year":"1998","journal-title":"Research Report 3487"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/EMRTS.2000.854003"},{"key":"ref2","article-title":"Model checking in dense real-time","author":"alur","year":"1991","journal-title":"Technical Report"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/3-540-61739-6_33","article-title":"Cache behavior prediction by abstract interpretation","volume":"11","author":"alt","year":"1996","journal-title":"Static Analysis Symposium (SAS)"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309989"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/EMRTS.2001.934025"},{"key":"ref21","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0057778","article-title":"Automatic accurate time-bound analysis for high-level languages","author":"liu","year":"1998","journal-title":"Languages Compilers and Tools for Embedded Systems (LCTES)"},{"year":"0","key":"ref42"},{"key":"ref24","first-page":"795","article-title":"Extending syn chronous languages for generating abstract real-time models","author":"logothetis","year":"2002","journal-title":"Design Automation and Test in Europe (DATE)"},{"key":"ref41","article-title":"Digital Design with Verilog HD","author":"sternheim","year":"1990","journal-title":"Automation Series"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2001.930720"},{"key":"ref26","article-title":"Exact low-level runtime analysis of synchronous programs for formal verification of real-time systems","author":"logothetis","year":"2003","journal-title":"Forum on Design Languages (FDL)"},{"key":"ref25","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1109\/DATE.2003.1186386","article-title":"Exact high level WCET analysis of synchronous programs by symbolic state space exploration","author":"logothetis","year":"2003","journal-title":"Design Automation and Test in Eu rope (DATE)"}],"event":{"name":"24th IEEE International Real-Time Systems Symposium","acronym":"REAL-03","location":"Cancun, Mexico"},"container-title":["Proceedings. 2003 International Symposium on System-on-Chip (IEEE Cat. No.03EX748)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8877\/28040\/01253272.pdf?arnumber=1253272","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,2]],"date-time":"2020-04-02T07:36:06Z","timestamp":1585812966000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1253272\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":42,"URL":"https:\/\/doi.org\/10.1109\/real.2003.1253272","relation":{},"subject":[]}}