Automatic Conversion Method of the Requirements Specification Verification for CTCS Level 3

Abstract:

Chinese Train Control System Level 3(CTCS-3) is a typical complex cyber-physical system which connects the control center, the station and the train. In order to ensure the friendly communication between the different manufacturers equipment, the high reliability is required by the CTCS-3 system. The reliability of a system can be tested with the formal verification method and a lot of formal tools have been developed, such as SPIN, VIS and NuSMV. In this paper, we describe the modeling techniques and abstractions of the control process. The required assembly unit has been specified as extended class. The required behavior has been specified as extended state machine diagrams and translated to temporal logic properties. Then, we propose a method to simplify the steps which transfer a UML model into a formal model. Moreover, the transition can be implemented with development language, where its result-the formal model-can be run by the formal tool and return an analysis result. At last, we take the Radio Block Center (RBC) Handover of CTCS-3 as an example, and the experimental results show the validity and feasibility of this method.

• Periodical: Applied Mechanics and Materials (Volume 563)
• Pages: 248-257
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.563.248
• Online since: May 2014
• Authors: Yu Ping Zhou*, Lin Zhao, Jin Tao Liu
• Keywords: CTCS-3, Formal Verification, NuSMV, Reliability

References

[1] TANG Tao, GAO Chun-hai. Analysis of ETCS system and study on CTCS . Electric Drive for Locomotives, 6(1), pages 1-3, (2004).

[2] Xie Yu-fei , TANG Tao, XU Tian-hua, ZHAO Lin. Research on Method of Modeling and Formal Verfication of the CTCS-3 Train Control System Specification , 铁道学报 [J], 2011, 33(7): 67-72.

[3] 吕继东, 唐涛, 贾昊. 客运专线CTCS-3级列控系统无线闭塞中心的建模与验证. 铁道学报[J], 2010, 32(6): 34-42.

DOI: 10.36012/etr.v2i4.1663

[4] 李宪. 基于UML的列控系统建模方法与验证工具集成. 北京: 北京交通大学硕士论文[D]. (2012).

DOI: 10.7498/aps.59.859

[5] K. M. Hansen. Validation of a railway interlocking model. In: Proceedings of FME'94: Industrial Benefit of Formal Methods. vol. 873 of of Lecture Notes in Computer Science, Springer, 1994, page: 582-601.

DOI: 10.1007/3-540-58555-9_117

[6] 刘金涛, 唐涛, 徐田华, 赵林. 基于UML的CTCS-3级别列控系统需求规范形式化验证方法. 中国铁道科学[J], 2011, 32(3): 93-99.

DOI: 10.1360/n112014-00017

[7] Ministry of Railways. CTCS-3 system requirements specification [M]. Beijing: China Railway Publishing House; (2009).

[8] 唐涛, 徐田华, 赵林. 列车运行控制规范[M]. 北京: 中国铁道出版社, 2010. 197.

[9] Roberto Cavada, Alessandro Cimatti, Charles Arthur Jochim, Gavin Keighren, Emanuele Olivetti, Marco Pistore, Marco Roveri and Andrei Tchaltsev. NuSMV 2. 5 User Manual, (2011).

[10] Xiang Gan, Jori Dubrovn, Keijio Heljanko. A symbolic model checking approach to verifying satellite onboard software. Science of Computer Programming[M], (2013).

DOI: 10.1016/j.scico.2013.03.005