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

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

基于规则的CTCS-1级列控系统RDC数据验证工具的设计和实现

区域列控数据中心(RDC)是CTCS-1级列控系统新增的地面核心设备,主要为车载设备提供线路数据、临时限速数据和进路数据。RDC子系统自带静态数据库,存储当前RDC管辖区域内的线路数据。本文在深入研究RDC数据特点的基础上,提取数据约束规则,并设计开发T RDC数据自动化验证工具,提高了数据验证的效率和准确率。