Formal Verification of Communication Based Train Control System
In the CBTC (Communication-based Train Control) system, the wireless terminals (repeaters) are the communication bridges between the control-center and the on-board system. This paper presents a formal analysis of the train-to-ground communication link verification (TCLV) system. Firstly, this paper lists the requirements and analyzes the necessary system state and operations, then transforms the natural language describing system into a rigorous mathematical described model. At last, for the formal model, the proof obligations are proved to verify its internal consistency, and the validations are proved to verify the states and operations satisfying the expected requirements. The result of proof denotes that the actual system designed as the specification described in this paper would satisfy the requirements under the premise of safety and reliability.
TCLV system formal methods ATP VDM railway system
Guo XIE Xinhong HEI Akira ASANO Hiroshi MOCHIZUKI Sei TAKAHASHI Hideo NAKAMURA
Department of Electronics and Computer Science College of Science and Technology Nihon University Fu School of Computer Science and Engineering Xi an University of Technology Xi an, China Railway Signal Division, Development Dept. Kyosan Electric MFG. CO., LTD Yokohama, Japan
国际会议
西安
英文
406-411
2011-06-17（万方平台首次上网日期，不代表论文的发表时间）