论文部分内容阅读
等级转换是高速铁路列车运行控制系统的一个主要运营场景。当列车通过CTCS-3级区域和CTCS-2级区域边界时,车载子系统、无线闭塞中心、司机、预告应答器以及转换应答器之间存在大量的信息交互过程,并对列车的安全运行和行车效率有直接的影响,因此有必要采取形式化建模方式对该过程进行分析和验证。文章根据时间自动机理论对CTCS-3级向CTCS-2级转换的过程进行建模,并应用UPPAAL对转换过程各子系统的信息交互一致性和实时性进行验证。结果表明,该过程满足交互一致性和实时性的规范要求。