Data validation of regional data center for CTCS-1 train control system based on CSP
-
摘要: 区域列控数据中心（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. -
-
[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
下载:
计量
- 文章访问数: 293
- HTML全文浏览量: 105
- PDF下载量: 36
