CTCS-3 级列控车载设备的形式化建模与验证

CTCS-3级列控系统安全苛求性较高,而列控车载设备是CTCS-3级列控系统的主体,主要功能是对列车进行操纵和控制,保证列车安全运行的关键。通过分析CTCS-3级列控车载设备之间的信息交互以及车载安全计算机中工作模式的转换规则,采用有色Petri网(CPN)建立车载设备的信息交互模型以及工作模式转换模型,使用ASK-CTL分支时序逻辑公式验证了模型的死标识、死锁以及分析工作模式下的系统行为等特性,验证构建的CPN模型符合系统规范要求的流程及规则,可为相关安全苛求系统的设计提供一定参考。