{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T04:29:51Z","timestamp":1729657791818,"version":"3.28.0"},"reference-count":30,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,3]]},"DOI":"10.1109\/date.2012.6176499","type":"proceedings-article","created":{"date-parts":[[2013,2,19]],"date-time":"2013-02-19T13:16:29Z","timestamp":1361279789000},"page":"370-375","source":"Crossref","is-referenced-by-count":7,"title":["State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems"],"prefix":"10.1109","author":[{"given":"M.","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Hartmanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K. G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Tretmans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","first-page":"416","article-title":"The bounded retransmission protocol must be on time!","volume":"1217","author":"d'argenio","year":"1997","journal-title":"LNCS"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21461-5_4"},{"key":"18","first-page":"127","article-title":"Proof-checking a data link protocol","volume":"806","author":"helmink","year":"1993","journal-title":"LNCS"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25271-6_20"},{"journal-title":"Implementation of Symbolic Model Checking for Probabilistic Systems","year":"2002","author":"parker","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_16"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2009.41"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.104"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"21","first-page":"3","article-title":"Modeling Heterogeneous Realtime Systems in BIP","author":"basu","year":"0","journal-title":"Software Engineering and Formal Methods SEFM'06 Proceedings 2006"},{"key":"20","first-page":"39","article-title":"Reachability analysis of probabilistic systems by successive refinements","volume":"2165","author":"d'argenio","year":"2001","journal-title":"LNCS"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"key":"23","first-page":"614","article-title":"D-Finder: A Tool for Compositional Deadlock Detection and Verification","author":"bensalem","year":"0","journal-title":"Computer- Aided Verification CAV'09 Proceedings 2009"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2010.2069102"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879049"},{"key":"26","first-page":"631","article-title":"Incremental Component-Based Construction and Verification of a Robotic System","author":"basu","year":"0","journal-title":"European Conference on Artificial Intelligence ECAI'08 Proceedings 2008"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22045-6_8"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78917-8_1"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04570-7_19"},{"key":"3","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","article-title":"Minimum-cost reachability for priced timed automata","volume":"2034","author":"behrmann","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032042"},{"key":"10","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/978-3-642-24310-3_7","article-title":"Statistical model checking for networks of priced timed automata","volume":"6919","author":"david","year":"2011","journal-title":"Lecture Notes in Computer Science"},{"key":"1","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","article-title":"A tutorial on uppaal","volume":"3185","author":"behrmann","year":"2004","journal-title":"Lecture Notes in Computer Science"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24431-5_10"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086283"},{"key":"6","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/978-3-642-00602-9_7","article-title":"Automatic synthesis of robust and optimal controllers - An industrial case study","volume":"5469","author":"cassez","year":"2009","journal-title":"Lecture Notes in Computer Science"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"4","first-page":"113","article-title":"Metamoc: Modular execution time analysis using model checking","volume":"15","author":"dalsgaard","year":"2010","journal-title":"OASICS"},{"key":"9","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","article-title":"Time for statistical model checking of real-time systems","volume":"6806","author":"david","year":"2011","journal-title":"Lecture Notes in Computer Science"},{"key":"8","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1145\/1755952.1755967","article-title":"Timed i\/o automata: A complete specification theory for real-time systems","author":"david","year":"2010","journal-title":"HSCC"}],"event":{"name":"2012 Design, Automation & Test in Europe Conference & Exhibition (DATE 2012)","start":{"date-parts":[[2012,3,12]]},"location":"Dresden","end":{"date-parts":[[2012,3,16]]}},"container-title":["2012 Design, Automation & Test in Europe Conference & Exhibition (DATE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6171057\/6176405\/06176499.pdf?arnumber=6176499","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T03:48:18Z","timestamp":1498016898000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6176499\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1109\/date.2012.6176499","relation":{},"subject":[],"published":{"date-parts":[[2012,3]]}}}