Modeling and Verification of Level Transition Scenario of Train Control System CTCS-1

doi:10.3778/j.issn.1002-8331.1807-0056

Abstract

Abstract: With the development of key technologies of the CTCS-1 train control system, it is inevitable that the trains carrying CTCS-1 control system will run across to the CTCS-0 level line, and the smooth implementation of the system level transition is the basis for safe cross-line operations. Based on the system function analysis, a multi-resolution function model is established to identify the scenario requirement of level transition. According to the scenario requirement and the exsisting system specifications, the scheme of CTCS-1 system level transition scenario is improved. A UML-based NuSMV modeling and verification method is used to establish the UML model and NuSMV model of level transition scenario. The activity, certainty and other properties of the scenario model are verified, which proves that the improved scenario meets the scenario requirements and the system specifications. The discussion of the CTCS-1 level transition scenario can support the revision of the relevant specifications.

Key words: CTCS-1 train control system, scenario of level transition, NuSMV model, verification

摘要： 随着CTCS-1级列控系统关键技术研究工作的开展，必然要面临装载CTCS-1级车载设备的列车跨线运营至CTCS-0级线路的问题，而系统等级转换的顺利进行是实现列车安全跨线运营的基础。通过系统功能分析，建立了系统多分辨率功能模型，以识别等级转换场景需求；根据场景需求，结合现行系统规范，完善了CTCS-1级系统等级转换场景的方案；采用基于UML的NuSMV建模与验证方法，建立了等级转换场景的UML模型和NuSMV模型，并验证了场景模型的活性、确定性等属性，从而证明了完善后的场景方案满足场景需求，且符合系统规范。文中对CTCS-1级系统等级转换场景的探讨可为相关规范的修订提供支持。

关键词: CTCS-1级列控系统, 等级转换场景, NuSMV模型, 模型验证

WANG Yingzhuo, LIU Zhongtian. Modeling and Verification of Level Transition Scenario of Train Control System CTCS-1[J]. Computer Engineering and Applications, 2019, 55(18): 256-262.

王颖卓，刘中田. CTCS-1级列控系统等级转换场景建模与验证[J]. 计算机工程与应用, 2019, 55(18): 256-262.

[1]	ZHENG Liang, CHEN Ya, CHEN Xiaopan, ZHENG Fengbin. Kinship Verification Method of Facial Local Feature Enhancement [J]. Computer Engineering and Applications, 2021, 57(23): 226-233.
[2]	LI Duo, DONG Chaoqun, SI Pinchao, HE Man, LIU Qianchao. Survey of Research on Neural Network Verification and Testing Technology [J]. Computer Engineering and Applications, 2021, 57(22): 53-67.
[3]	TAN Lijuan, ZHENG Wei, LIU Youlin, FAN Xin, YANG Fengyu. Survey of Airborne Software Test and Verification Methods for Airworthiness Standards [J]. Computer Engineering and Applications, 2021, 57(15): 9-22.
[4]	LIU Youlin, ZHENG Wei, TAN Lijuan, FAN Xin, YANG Fengyu. Summary of Airborne Software Testing and Verification Tools for Airworthiness Standards [J]. Computer Engineering and Applications, 2021, 57(11): 1-10.
[5]	TANG Dengping, CAI Wenjia, ZOU Li, HU Xiang, DING Li, WANG Xue. Application of Improved Convolution Neural Network in Fault Diagnosis of Transformer [J]. Computer Engineering and Applications, 2021, 57(11): 239-247.
[6]	WU Jie, DUAN Jin, DONG Suoqin, LI Yingchao. Research on Face Recognition Technology of DFM-GAN Network in Cross-Age Simulation [J]. Computer Engineering and Applications, 2021, 57(10): 117-124.
[7]	XIE Yifei, LU Qi, LIU Xin, HU Yahao, PAN Zhisong, CHEN Hao. Graph-Based Hierarchical Attention Networks for Fact Verification [J]. Computer Engineering and Applications, 2021, 57(10): 146-153.
[8]	WANG Fusen, LI Zhihuai, TIAN Na. Multiple Rounds of PBFT Verification Scheme to Improve Scale and Validity of Sharding [J]. Computer Engineering and Applications, 2020, 56(24): 102-108.
[9]	CHEN Hong, ZHU Yanan, XIAO Chenglong, JIN Haibo, ZHANG Zihao. Publicly Verifiable Certificateless Multi-receiver Anonymous Signcryption [J]. Computer Engineering and Applications, 2020, 56(19): 120-125.
[10]	SHE Xiangyang, LIU Qiao, YE Ou. Research on Face Verification Algorithm Based on LeNet-5 and Siamese Neural Network Model [J]. Computer Engineering and Applications, 2020, 56(15): 215-220.
[11]	ZHANG Guipeng, KUANG Zhenxi, CHEN Pinghua. Cloud Storage Deduplication Scheme Using Signature and Hash Technology [J]. Computer Engineering and Applications, 2020, 56(1): 76-82.
[12]	YIN Jianjin1, ZHANG Beike1, GAO Dong1, XU Xin2. Improved Bat Algorithm for Solving Flexible Flow Shop Scheduling Problem and Its Application [J]. Computer Engineering and Applications, 2019, 55(9): 243-247.
[13]	ZHANG Shuai, YAN An, JIA Minzhi. Crowdfunding Smart Contract Design Based on Blockchain Technology [J]. Computer Engineering and Applications, 2019, 55(8): 220-225.
[14]	FENG Fujian. Verification Analysis for Delay Time Petri Nets [J]. Computer Engineering and Applications, 2019, 55(4): 72-78.
[15]	HU Zhengping, LIU Huaibiao, SUN Degang. Kinship Verification Based on Neighborhood Repulsed Metric Sparse Discriminant for Single Sample [J]. Computer Engineering and Applications, 2019, 55(22): 133-139.

Modeling and Verification of Level Transition Scenario of Train Control System CTCS-1

CTCS-1级列控系统等级转换场景建模与验证

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics