{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T11:44:00Z","timestamp":1762429440658,"version":"3.37.3"},"reference-count":40,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"National Key Research and Development Program of China","award":["2018YFB2101300"],"award-info":[{"award-number":["2018YFB2101300"]}]},{"DOI":"10.13039\/501100001809","name":"Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61872147"],"award-info":[{"award-number":["61872147"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004106","name":"East China Normal University Academic Innovation Promotion Program for Excellent Doctoral Students","doi-asserted-by":"publisher","award":["YBNLTS2020-041"],"award-info":[{"award-number":["YBNLTS2020-041"]}],"id":[{"id":"10.13039\/501100004106","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2020,11]]},"DOI":"10.1109\/tcad.2020.3012843","type":"journal-article","created":{"date-parts":[[2020,10,2]],"date-time":"2020-10-02T20:24:18Z","timestamp":1601670258000},"page":"4006-4017","source":"Crossref","is-referenced-by-count":10,"title":["Quantitative Timing Analysis for Cyber-Physical Systems Using Uncertainty-Aware Scenario-Based Specifications"],"prefix":"10.1109","volume":"39","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5058-4660","authenticated-orcid":false,"given":"Ming","family":"Hu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenxue","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1938-2902","authenticated-orcid":false,"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7421-1711","authenticated-orcid":false,"given":"Tongquan","family":"Wei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3922-0989","authenticated-orcid":false,"given":"Mingsong","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","first-page":"349","article-title":"Time for statistical model checking of real-time systems","author":"david","year":"2004","journal-title":"Proc Int Conf Comput Aided Verification (CAV)"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.108.2"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/TSUSC.2017.2723500"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2591062.2591132"},{"key":"ref31","first-page":"204","article-title":"Model checking time-constrained scenario-based specifications","author":"akshay","year":"2010","journal-title":"Proc Foundations of Software Technology and Theoretical Computer Science"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_56"},{"year":"2015","key":"ref37","article-title":"OMG unified modeling language TM (OMG UML), superstructure version 2.5"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/11951148_6"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.3850\/9783981537079_0339"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_24"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2661665"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177706645"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2012.27"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21393-9_4"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0239-9"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3195013"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568239"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2012.07.017"},{"key":"ref18","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","article-title":"Statistical model checking of black-box probabilistic systems","author":"sen","year":"2004","journal-title":"Proc Int Conf Comput Aided Verification (CAV)"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38613-8_11"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2008.9"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-017-0609-6"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35271-8_6"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106299"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_1"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1002\/stv.434"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227159"},{"journal-title":"The Unified Modeling Language User Guide","year":"2005","author":"booch","key":"ref8"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-017-0594-9"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2016.2633961"},{"journal-title":"The Unified Modeling Language Reference Manual","year":"2004","author":"rumbaugh","key":"ref9"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.25"},{"key":"ref20","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","article-title":"Uppaal SMC tutorial","volume":"17","author":"david","year":"2015","journal-title":"Int J Softw Tools Technol Transfer (STTT)"},{"journal-title":"Message Sequence Chart (MSC)","year":"2011","key":"ref22"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24310-3_7"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.034"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BF02802920"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503220"},{"key":"ref25","first-page":"73","article-title":"A model checking based approach for containment checking of UML sequence diagrams","author":"muram","year":"2015","journal-title":"Proc Asia-Pacific Software Engineering Conf (APSEC) '95"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/9244237\/09211563.pdf?arnumber=9211563","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,27]],"date-time":"2022-04-27T14:04:54Z","timestamp":1651068294000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9211563\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11]]},"references-count":40,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2020.3012843","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"type":"print","value":"0278-0070"},{"type":"electronic","value":"1937-4151"}],"subject":[],"published":{"date-parts":[[2020,11]]}}}