{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:07:49Z","timestamp":1753884469782,"version":"3.41.2"},"reference-count":21,"publisher":"Wiley","issue":"1","license":[{"start":{"date-parts":[[2018,6,4]],"date-time":"2018-06-04T00:00:00Z","timestamp":1528070400000},"content-version":"vor","delay-in-days":154,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61603026"],"award-info":[{"award-number":["61603026"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005089","name":"Beijing Municipal Natural Science Foundation","doi-asserted-by":"publisher","award":["L171004"],"award-info":[{"award-number":["L171004"]}],"id":[{"id":"10.13039\/501100005089","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["onlinelibrary.wiley.com"],"crossmark-restriction":true},"short-container-title":["Wireless Communications and Mobile Computing"],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>VBTC (vehicle\u2010to\u2010vehicle communication based train control) has gradually become an important research trend in the field of rail transit. This has resulted in advantages of decreasing the number of pieces of wayside equipment and improving the efficiency of real\u2010time system communication. Characteristics and mechanism of train\u2010to\u2010train communication, as key implementation technology of safety critical system, are given and discussed. A new method, based on the LTS (labelled transition system) model checking, is proposed for verifying the safety properties in the communication procedure. The LTS method is adapted to model system behaviours; analysis and safety verification are checked by means of LTSA (labelled transition system analyzer) software. The results show that it is an efficient method to verify safety properties, as well as to assist the complex system\u2019s design and development.<\/jats:p>","DOI":"10.1155\/2018\/2406968","type":"journal-article","created":{"date-parts":[[2018,6,4]],"date-time":"2018-06-04T23:30:51Z","timestamp":1528155051000},"update-policy":"https:\/\/doi.org\/10.1002\/crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Study on Formal Modeling and Safety Verification of Train\u2010to\u2010Train Communication"],"prefix":"10.1155","volume":"2018","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7279-9390","authenticated-orcid":false,"given":"Haonan","family":"Feng","sequence":"first","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2018,6,4]]},"reference":[{"key":"e_1_2_9_1_2","doi-asserted-by":"publisher","DOI":"10.3969\/j.issn.1001-8360.2017.02.001"},{"key":"e_1_2_9_2_2","doi-asserted-by":"crossref","unstructured":"ZhuL. YuF. R. andNingB. An optimal handoff decision algorithm for Communication-Based Train Control (CBTC) systems Proceedings of the 2010 IEEE Vehicular Technology Conference (VTC 2010-Fall) September 2010 Ottawa ON Canada 1\u20135 https:\/\/doi.org\/10.1109\/VETECF.2010.5594428.","DOI":"10.1109\/VETECF.2010.5594428"},{"key":"e_1_2_9_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2012.120506"},{"key":"e_1_2_9_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2014.2298409"},{"key":"e_1_2_9_5_2","doi-asserted-by":"publisher","DOI":"10.1186\/1687-1499-2012-211"},{"key":"e_1_2_9_6_2","first-page":"78","article-title":"Analysis of novel CBTC system based on train to train communication","volume":"50","author":"Xu J. K.","year":"2014","journal-title":"Railway Signaling and Communication"},{"key":"e_1_2_9_7_2","unstructured":"LiC. Research on Train Communication Cooperation under V2V Communication Environment based on State Machine 2017 Beijing Jiaotong University Master Degree."},{"key":"e_1_2_9_8_2","first-page":"91","article-title":"A new generation of CBTC system without CI and ZC","volume":"30","author":"Du H.","year":"2017","journal-title":"Urban Rapid Rail Transit"},{"key":"e_1_2_9_9_2","first-page":"23","article-title":"Alstrom\u2032s simplified CBTC technology to debut in lille","volume":"53","author":"Briginshaw D.","year":"2013","journal-title":"International Railway Journal"},{"key":"e_1_2_9_10_2","first-page":"91","article-title":"Formal dynamic operational model of RIS components","volume":"11","author":"Zafar N.","year":"2011","journal-title":"International Journal of Computer Science and Network Security"},{"key":"e_1_2_9_11_2","first-page":"57","article-title":"Research on event-B based modelling and verification of interlocking route control","volume":"22","author":"Tong H. D.","year":"2013","journal-title":"Railway Computer Application"},{"key":"e_1_2_9_12_2","doi-asserted-by":"crossref","unstructured":"ZafarN. A. Formal model for moving block railway interlocking system based on un-directed topology Proceedings of the 2nd Annual International Conference on Emerging Techonologies 2006 ICET 2006 November 2006 Peshawar Pakistan 217\u2013223 https:\/\/doi.org\/10.1109\/ICET.2006.335983 2-s2.0-46149127088.","DOI":"10.1109\/ICET.2006.335983"},{"key":"e_1_2_9_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2017.03.001"},{"key":"e_1_2_9_14_2","doi-asserted-by":"publisher","DOI":"10.3182\/20090610-3-IT-4004.00039"},{"key":"e_1_2_9_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48118-4_58"},{"key":"e_1_2_9_16_2","first-page":"193","article-title":"Method for generating formal interlocking software model based on scenario","volume":"42","author":"Dong Y.","year":"2015","journal-title":"Computer Science"},{"key":"e_1_2_9_17_2","doi-asserted-by":"publisher","DOI":"10.3969\/j.issn.1001-8360.2016.11.012"},{"key":"e_1_2_9_18_2","first-page":"156","article-title":"A software safety verification method based on model checking","volume":"56","author":"Wang X.","year":"2010","journal-title":"Journal of Wuhan University (Natural Science Edition)"},{"key":"e_1_2_9_19_2","doi-asserted-by":"publisher","DOI":"10.1504\/IJCAT.2013.052795"},{"key":"e_1_2_9_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.trc.2014.02.002"},{"volume-title":"Concurrency State Models and Java Programs","year":"1999","author":"Magee J.","key":"e_1_2_9_21_2"}],"container-title":["Wireless Communications and Mobile Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/wcmc\/2018\/2406968.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/wcmc\/2018\/2406968.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1155\/2018\/2406968","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T06:47:31Z","timestamp":1723013251000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1155\/2018\/2406968"}},"subtitle":[],"editor":[{"given":"Li","family":"Zhu","sequence":"additional","affiliation":[]}],"short-title":[],"issued":{"date-parts":[[2018,1]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1155\/2018\/2406968"],"URL":"https:\/\/doi.org\/10.1155\/2018\/2406968","archive":["Portico"],"relation":{},"ISSN":["1530-8669","1530-8677"],"issn-type":[{"type":"print","value":"1530-8669"},{"type":"electronic","value":"1530-8677"}],"subject":[],"published":{"date-parts":[[2018,1]]},"assertion":[{"value":"2017-12-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-04-23","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-06-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"2406968"}}