{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T09:27:45Z","timestamp":1761989265881,"version":"3.37.3"},"reference-count":35,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"National Key Research and Development Project","award":["2017YFB1001800"],"award-info":[{"award-number":["2017YFB1001800"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61620106007","61332008","61572195","61802251"],"award-info":[{"award-number":["61620106007","61332008","61572195","61802251"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Defense Industrial Technology Development Program of China","award":["JCKY2016212B004-2"],"award-info":[{"award-number":["JCKY2016212B004-2"]}]},{"name":"SAUSE: Secure, Adaptive, Usable Software Engineering (EPSRC Platform)","award":["EP\/R013144\/1"],"award-info":[{"award-number":["EP\/R013144\/1"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Intell. Transport. Syst."],"published-print":{"date-parts":[[2018,11]]},"DOI":"10.1109\/tits.2018.2869633","type":"journal-article","created":{"date-parts":[[2018,10,4]],"date-time":"2018-10-04T19:13:05Z","timestamp":1538680385000},"page":"3517-3528","source":"Crossref","is-referenced-by-count":13,"title":["Simplifying the Formal Verification of Safety Requirements in Zone Controllers Through Problem Frames and Constraint-Based Projection"],"prefix":"10.1109","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6536-5746","authenticated-orcid":false,"given":"Zhengheng","family":"Yuan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaohong","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jing","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yijun","family":"Yu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haiying","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3882-8025","authenticated-orcid":false,"given":"Tingliang","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1087-226X","authenticated-orcid":false,"given":"Zhi","family":"Jin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","volume":"2","author":"jones","year":"1990","journal-title":"Systematic Software Development Using VDM"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58555-9_117"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48118-4_58"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/32.879808"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-016-0517-1"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.23940\/ijpe.17.06.p11.897912"},{"journal-title":"Problem Frames Analyzing and Structuring Software Development Problems","year":"2001","author":"jackson","key":"ref10"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194016500029"},{"year":"0","key":"ref12"},{"journal-title":"Language Reference Manual","year":"2013","key":"ref13"},{"article-title":"Symbolic model checking: An approach to the state explosion problem","year":"1992","author":"mcmillan","key":"ref14"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2009.22"},{"journal-title":"Environment Modeling-Based Requirements Engineering for Software Intensive Systems","year":"2018","author":"jin","key":"ref16"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2016.182"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76719-0_38"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2010.58"},{"key":"ref28","first-page":"236","article-title":"A method to model guidelines for developing railway safety-critical systems with UML","author":"ossami","year":"2007","journal-title":"ICSOFT (SE)"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050022"},{"key":"ref27","first-page":"275","article-title":"Learning-based compositional model checking of behavioral UML systems","author":"meller","year":"2015","journal-title":"Proc Int'l Workshop Formal Aspects of Component Software"},{"journal-title":"Railway Application—Communications Signaling and Processing Systems—Safety Related Electronic Systems for Signaling","year":"2003","key":"ref3"},{"key":"ref6","first-page":"2","article-title":"SCADE: A comprehensive framework for critical system and software engineering","author":"le sergent","year":"2011","journal-title":"Proc of the SDL Forum"},{"journal-title":"Concurrency State Models and Java Programs","year":"1999","author":"magee","key":"ref29"},{"key":"ref5","first-page":"115","article-title":"Designing safe, reliable systems using SCADE","author":"abdulla","year":"2004","journal-title":"Proc Int Symp Leveraging Appl Formal Methods Verification Validation"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2004.95746"},{"article-title":"Modeling and safety verification of zone controller in CBTC with UML","year":"2008","author":"yang","key":"ref7"},{"journal-title":"Railway Applications—Communication Signaling and Processing Systems—Software for Railway Control and Protection Systems","year":"2011","key":"ref2"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2015.10"},{"key":"ref1","first-page":"369","article-title":"Météor: A successful application of B in a large project","author":"behm","year":"1999","journal-title":"Proc Int Symp Formal Methods"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6_3"},{"article-title":"Verification and planning for stochastic processes with asynchronous events","year":"2005","author":"younes","key":"ref22"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","article-title":"Applying SAT methods in unbounded symbolic model checking","volume":"2","author":"mcmillan","year":"2002","journal-title":"Computer Aided Verification—CAV"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","article-title":"Microarchitecture verification by compositional model checking","author":"jhala","year":"2001","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39190"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_39"},{"key":"ref25","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","article-title":"Parameterized verification of the FLASH cache coherence protocol by compositional model checking","author":"mcmillan","year":"2001","journal-title":"Correct Hardware Design and Verification Methods"}],"container-title":["IEEE Transactions on Intelligent Transportation Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6979\/8529280\/08481403.pdf?arnumber=8481403","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T18:27:04Z","timestamp":1643221624000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8481403\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":35,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tits.2018.2869633","relation":{},"ISSN":["1524-9050","1558-0016"],"issn-type":[{"type":"print","value":"1524-9050"},{"type":"electronic","value":"1558-0016"}],"subject":[],"published":{"date-parts":[[2018,11]]}}}