基于MSC与UPPAAL的高铁跨界临时限速建模与验证

摘要

Temporary Speed Restriction Server ( TSRS) is an important part of the High Speed Railway Train Control System, it not only checks the temporary speed restriction orders issued by CTC, but also exchanges information frequently with the temporary speed restriction server of the adjacent dispatching station, and the requirements for its security and real-time performance are rigorous. In order to meet the requirement of the high speed railway train control system, a combination of timed automata theory with Message Sequence Chart ( MSC ) is employed to establish firstly the MSC model of Cross-border Temporary Speed Restriction and timed automata submodel, and then the verification tool of UPPAAL is used to verify the properties of the Cross-border Temporary Speed Restriction System described by BNF syntax. According to the simulation verification results, the security and restricted activity of the Cross-border Temporary Speed Restriction Information are confirmed, which provides an important basis for further development of the Temporary Speed Restriction Server.%临时限速服务器是高铁列控系统的重要组成部分，其不仅要校验CTC下发的临时限速命令，还要与相邻调度台临时限速服务器之间进行频繁的信息交互，因此对其安全性和实时性要求也更苛刻。为了满足高铁列控系统对其运行的要求，采用时间自动机理论和消息顺序图( MSC)相结合的方法，首先建立跨界临时限速命令的MSC模型和时间自动机子模型，再利用UPPAAL验证工具对形式化语法BNF描述的时间自动机子模型属性进行验证。根据仿真验证结果确认了跨界临时限速信息的安全性和受限活性，为进一步开发临时限速服务器功能提供了重要的依据。