DocumentCode :
2387876
Title :
Formalizing and Analyzing the Train-to-Wayside Network System for CBTC
Author :
Guo Xie ; Xinhong Hei ; Mochizuki, H. ; Takahashi, S. ; Nakamura, H.
Author_Institution :
Xi´an Univ. of Technol., Xi´an, China
fYear :
2012
fDate :
18-19 Nov. 2012
Firstpage :
15
Lastpage :
22
Abstract :
In the development of communication based train control (CBTC) system, while communicating with the control center, the train must be assigned accurately to the wayside network. In order to verify the rigor of this process, the specification is analyzed formally in this paper. After studying the system, the functional requirements are clarified firstly. Followed by the formal specification is established by VDM explicitly, including the state variables and top-level operations. Then the internal consistence of the formal specification is validated, which can prevent potential runtime errors in software program. Lastly, in order to ensure that the specification satisfies requirements, the requirements are transformed to corresponding inference rules, and then validated by discharging proof obligations. The work in this paper indicates that if the software system of a CBTC system is designed strictly in accordance with the specification, it will be internal consistent with high reliability, and satisfy the design requirements.
Keywords :
control engineering computing; formal specification; inference mechanisms; railway communication; railways; CBTC; VDM; communication based train control system; design requirements; formal specification; inference rules; proof obligations; software program; train-to-wayside network system;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Dependable Transportation Systems/Recent Advances in Software Dependability (WDTS-RASD), 2012 Workshop on
Conference_Location :
Niigata
Print_ISBN :
978-1-4799-0315-3
Type :
conf
DOI :
10.1109/WDTS-RASD.2012.13
Filename :
6532143
Link To Document :
بازگشت