{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T14:16:22Z","timestamp":1761401782319},"reference-count":35,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1109\/rtas.2016.7461337","type":"proceedings-article","created":{"date-parts":[[2016,4,28]],"date-time":"2016-04-28T16:18:27Z","timestamp":1461860307000},"page":"1-11","source":"Crossref","is-referenced-by-count":20,"title":["From Stateflow Simulation to Verified Implementation: A Verification Approach and A Real-Time Train Controller Design"],"prefix":"10.1109","author":[{"given":"Yu","family":"Jiang","sequence":"first","affiliation":[]},{"given":"Yixiao","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Han","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Hui","family":"Kong","sequence":"additional","affiliation":[]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[]},{"given":"Jiaguang","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Lui","family":"Sha","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref33","article-title":"Synchronous Design and Verification of Critical Embedded Systems Using SCADE and Esterel","author":"berry","year":"2007","journal-title":"Formal Methods for Industrial Critical Systems"},{"journal-title":"Design of mixed synchronous\/asynchronous systems with multiple clocks","year":"2014","author":"jiang","key":"ref32"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2013.89"},{"journal-title":"Train Communication Network","article-title":"Iec 61375","year":"0","key":"ref30"},{"key":"ref35","article-title":"An Open Alternative for SMT-Based Verification of SCADE Models","author":"basoldet","year":"0","journal-title":"Proceedings of the Formal Methods for Industrial Critical Systems"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/COUFLESS.2015.15"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291172"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/CMPASS.1996.507891"},{"article-title":"Applied dynamics international","year":"0","author":"tester","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_19"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1450058.1450071"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63141-0_10"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1175\/2008MWR2415.1"},{"key":"ref28","first-page":"20","article-title":"Using simplicity to control complexity","author":"sha","year":"2001","journal-title":"IEEE Software"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2008.43"},{"journal-title":"Simulink","year":"0","key":"ref3"},{"year":"0","key":"ref6","article-title":"Stateflow user guide"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2889160.2889233"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297069"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_3"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0235-0"},{"journal-title":"SimulinkDesign Verifier","year":"0","key":"ref2"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/780732.780754"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2012.25"},{"journal-title":"UIUC","year":"0","author":"yu","key":"ref22"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2584651"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_18"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_36"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68524-1_3"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/11687061_6"}],"event":{"name":"2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)","start":{"date-parts":[[2016,4,11]]},"location":"Vienna, Austria","end":{"date-parts":[[2016,4,14]]}},"container-title":["2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7460013\/7461311\/07461337.pdf?arnumber=7461337","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,9,29]],"date-time":"2016-09-29T12:48:10Z","timestamp":1475153290000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7461337\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4]]},"references-count":35,"URL":"https:\/\/doi.org\/10.1109\/rtas.2016.7461337","relation":{},"subject":[],"published":{"date-parts":[[2016,4]]}}}