{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T01:53:46Z","timestamp":1649210026898},"reference-count":16,"publisher":"World Scientific Pub Co Pte Lt","issue":"03","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2014,4]]},"abstract":"<jats:p> This paper proposes a novel strategy for formally analyzing functional requirements specification (FRS) and applies it to the Automatic Train Protection and Block (ATPB) system, which is proposed to reconstruct conventional rail lines in Japan. Based on the FRS in natural language, firstly, dynamic state transitions are extracted to express the operational mechanisms and determine the system parameters. A complete model of the ATPB system is then established using Unified Modeling Language (UML) to express the system structure graphically and explicitly. After achieving a common understanding, a VDM++ model is established formally to redescribe the original FRS of the ATPB system which is written in natural language (i.e. Japanese). Following that, in order to ensure internal consistency of the specification, proof obligations of the VDM++ model are discharged. Furthermore, a comprehensive testing is implemented to ensure that the FRS meets actual requirements. Finally, the system is simulated strictly in accordance with the formal specification. Without any runtime errors, collisions or derailments, the results of the simulation demonstrate the high quality and safety of the specification. <\/jats:p>","DOI":"10.1142\/s0218194014500181","type":"journal-article","created":{"date-parts":[[2014,7,24]],"date-time":"2014-07-24T07:29:34Z","timestamp":1406186974000},"page":"465-492","source":"Crossref","is-referenced-by-count":1,"title":["A Strategy to Formalize Specification and Its Application to an Advanced Railway System"],"prefix":"10.1142","volume":"24","author":[{"given":"Guo","family":"Xie","sequence":"first","affiliation":[{"name":"Xi'an University of Technology, Xi'an Shaanxi 710048, China"},{"name":"State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University 100044, China"}]},{"given":"Xinhong","family":"Hei","sequence":"additional","affiliation":[{"name":"Xi'an University of Technology, Xi'an Shaanxi 710048, China"}]},{"given":"Sei","family":"Takahashi","sequence":"additional","affiliation":[{"name":"Department of Electronics and Computer Science, College of Science and Technology, Nihon University, 7-24-1 Narashinodai, Funabashi, Chiba 274-8501, Japan"}]},{"given":"Hideo","family":"Nakamura","sequence":"additional","affiliation":[{"name":"Department of Electronics and Computer Science, College of Science and Technology, Nihon University, 7-24-1 Narashinodai, Funabashi, Chiba 274-8501, Japan"}]}],"member":"219","published-online":{"date-parts":[[2014,7,24]]},"reference":[{"key":"rf1","first-page":"6","volume":"17","author":"Nakamura H.","year":"2011","journal-title":"Rolling Stock & Technology"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1541\/ieejias.131.914"},{"key":"rf3","first-page":"17","volume":"12","author":"Asano A.","year":"2012","journal-title":"IEEJ-ITS"},{"key":"rf4","doi-asserted-by":"publisher","DOI":"10.1109\/32.210303"},{"key":"rf6","unstructured":"A.\u00a0van Lamsweerde, The Future of Software Engineering, ed. A.\u00a0Finkelstein (ACM Press, 2000)\u00a0pp. 149\u2013159."},{"key":"rf9","doi-asserted-by":"publisher","DOI":"10.1007\/BF03192554"},{"key":"rf14","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Daniel J.","year":"2006"},{"key":"rf16","first-page":"557","volume":"28","author":"Hei X.","year":"2006","journal-title":"Journal of Reliability Engineering Association of Japan"},{"key":"rf17","first-page":"343","volume":"3","author":"Kurita T.","year":"2009","journal-title":"Intl. Journal of Software and Informatics"},{"key":"rf19","volume-title":"UML Distilled: A Brief Guide to the Standard Object Modeling Language","author":"Fowler M.","year":"2004"},{"key":"rf22","first-page":"671","volume":"2","author":"He Y.","year":"2006","journal-title":"Software Engineering Research and Practice"},{"key":"rf23","volume-title":"Validated Designs for Object-Oriented Systems","author":"Fitzgerald J.","year":"2005"},{"key":"rf25","first-page":"3","volume":"43","author":"Fitzgerald J.","year":"2008","journal-title":"SIGPLAN Notices"},{"key":"rf30","doi-asserted-by":"publisher","DOI":"10.1002\/0471734322"},{"key":"rf34","volume-title":"Train Control","author":"Nakamura H.","year":"2010"},{"key":"rf35","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194014500181","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T17:48:27Z","timestamp":1565200107000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194014500181"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4]]},"references-count":16,"journal-issue":{"issue":"03","published-online":{"date-parts":[[2014,7,24]]},"published-print":{"date-parts":[[2014,4]]}},"alternative-id":["10.1142\/S0218194014500181"],"URL":"https:\/\/doi.org\/10.1142\/s0218194014500181","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4]]}}}