基于CSP的CTCS-1级列控系统RDC数据验证的研究

卢铃冉; 张勇

基于CSP的CTCS-1级列控系统RDC数据验证的研究

卢铃冉,
张勇

北京交通大学电子信息工程学院，北京 100044

基金项目:

国家自然科学基金重点项目 6149700015

中国铁路总公司科技研究开发计划 2015X002-A

详细信息

作者简介:
卢铃冉，在读硕士研究生

张勇，副教授

中图分类号: U284.482:TP39
计量
- 文章访问数: 295
- HTML全文浏览量: 105
- PDF下载量: 36
出版历程
- 收稿日期: 2018-08-19
- 刊出日期: 2019-07-24

Data validation of regional data center for CTCS-1 train control system based on CSP

School of Electronic and Information Engineering, Beijing Jiaotong University, Beijing 100044, China

摘要

摘要: 区域列控数据中心（RDC）作为CTCS-1级列控系统地面设备的核心部分，为车载设备提供线路数据、临时限速信息、进路信息等，因此，RDC数据的正确性对列车正常运行至关重要。通过对RDC所包含的静态数据进行分析，总结出数据应满足的约束条件，以轨道区段数据为例，基于实体数据应满足的域值条件以及数据之间的关系建立数据约束规则，将数据验证规则加入数据验证流程，利用通信顺序进程（CSP）形式化语言对数据验证流程进行建模，用模型检验工具ProB对CSP语义模型进行检验。验证结果正确，表明数据验证方法可行，为RDC静态数据自动化验证奠定了基础。
- CTCS-1 /
- 区域列控数据中心(RDC) /
- 数据验证 /
- 通信顺序进程(CSP)
Abstract: The Regional Data Center (RDC), as the core trackside equipment of CTCS-1 train control system, provides track data, temporary speed restriction, and route information to the on-board equipment. Therefore, the correctness of RDC data is crucial to train operation safety. In this paper, the static data stored in RDC were analyzed and the constraints for them were summarized. Taking the track section data as an example, the data constraint rules were established based on the domain value conditions for entity data and the relationship between the data, the data validation rules were added into the data validation process which was modelled by using the communication sequence process (CSP) formal language. Finally, the model checker ProB was used to check the correctness of the CSP semantic models. The validation results are correct, which shows that the data validation method is feasible and lays a foundation for the automatic verification of RDC static data.
- CTCS-1 /
- regional data center (RDC) /
- data validation /
- communication sequence process (CSP)

HTML全文

图 1 RDC静态数据类图

下载: 全尺寸图片幻灯片

图 2 RDC数据验证流程建模与验证框图

下载: 全尺寸图片幻灯片

图 3 LTL语句部分约束规则验证结果

下载: 全尺寸图片幻灯片

参考文献(10)

[1]	莫志松. CTCS-1级列控系统总体技术方案探讨[J].中国铁路, 2016, (8): 37-43. https://www.cnki.com.cn/Article/CJFDTOTAL-TLZG201608009.htm
[2]	Storey, N. and A.Fanlkner. The Characteristics of Data in DataInetensive Safety-Related Systemes[C]//22nd Int.Conf.on ComputerSafety and Reliability, Safecomp 2003, Edinburgh, September 2003, pp.396-409.
[3]	Storey, N. and A.Fanlkner. Data Management in DataDriven Safety-Related Systems Proc[C]//20th Systems Safety Conference, Denver, CO., August 2002, 466-475.
[4]	Huber M, King S. Towards an Integrated Model Checker for Railway Signalling Data[C]// FME 2002: Formal MethodsGetting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings. DBLP, 2002: 204-223.
[5]	黄友能.城轨CBTC系统数据的安全处理与验证方法研究[D].北京: 北京交通大学, 2014.
[6]	中华人民共和国铁道部.列车运行监控装置(LKJ)数据文件编制规范(V1.0)[M].北京:中国铁道出版社, 2008.
[7]	Ryan P, Schneider S. The modelling and analysis of security protocols: the csp approach[M]. Addison-Wesley, 2001:261-265.
[8]	Leuschel M, Butler M. FME 2003: Formal Methods[M]. Springer Berlin Heidelberg, 2003:855-874.
[9]	陈倩佳, 卢佩玲.列控工程数据自动审核的研究与实现[J].铁路计算机应用, 2015, 24(3): 6-9. http://tljsjyy.xml-journal.net/article/id/3741
[10]	程忆佳, 王俊峰.列控数据完备性建模方法研究[J].铁路计算机应用, 2012, 21(7): 12-15. http://tljsjyy.xml-journal.net/article/id/826

施引文献(11)

期刊类型引用(6)

1.	代明智，王雷，覃天意. 基于参数化组件的道路BIM模型建模技术研究. 工程技术研究. 2024(02): 211-213 . 百度学术
2.	苏高飞，梁耀，侯亚博. 基于Civil 3D部件编辑器的矿山排土场参数化设计研究. 现代矿业. 2024(02): 100-103 . 百度学术
3.	李聪旭，徐晓磊，王雪甜，刘唯佳，焦雯雯. 基于BIM+GIS的铁路三维信息实景化技术研究. 铁道运输与经济. 2024(05): 100-109+117 . 百度学术
4.	梁建波. Civil3d部件编辑器关键技术应用研究. 水利技术监督. 2024(07): 252-254+270+277 . 百度学术
5.	张成，王双. 基于Civil 3D的河道设计软件开发及应用. 水利技术监督. 2022(11): 59-62 . 百度学术
6.	杨文成. 基于BIM设计的道岔设备建模方法研究. 铁道勘察. 2020(01): 133-136 . 百度学术