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

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

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

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.