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

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

作　　者：卢铃冉 张勇[1] LU Lingran;ZHANG Yong(School of Electronic and Information Engineering,Beijing Jiaotong University,Beijing 100044,China)

机构地区：[1]北京交通大学电子信息工程学院

出　　处：《铁路计算机应用》2019年第7期52-58,共7页Railway Computer Application

基　　金：国家自然科学基金重点项目(6149700015);中国铁路总公司科技研究开发计划(2015X002-A)

摘　　要：区域列控数据中心(RDC)作为CTCS-1级列控系统地面设备的核心部分,为车载设备提供线路数据、临时限速信息、进路信息等,因此,RDC数据的正确性对列车正常运行至关重要。通过对RDC所包含的静态数据进行分析,总结出数据应满足的约束条件,以轨道区段数据为例,基于实体数据应满足的域值条件以及数据之间的关系建立数据约束规则,将数据验证规则加入数据验证流程,利用通信顺序进程(CSP)形式化语言对数据验证流程进行建模,用模型检验工具ProB对CSP语义模型进行检验。验证结果正确,表明数据验证方法可行,为RDC静态数据自动化验证奠定了基础。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 区域列控数据中心(RDC) 数据验证 通信顺序进程(CSP) 

分 类 号：U284.482[交通运输工程—交通信息工程及控制] TP39[交通运输工程—道路与铁道工程]