CTCS-3级列控系统临时限速服务器建模与形式化验证

Modeling and Formal Verification of Temporary Speed Restriction Server for CTCS Level 3

临时限速服务器是CTCS-3级列控系统的重要组成部分,其系统安全性直接影响到高速铁路的运营安全。在TSRS系统研发过程中需对系统进行仿真建模和验证,发现系统设计错误,以保证系统的安全性。分析CTCS-3级列控系统临时限速服务器的组成结构,提取系统功能和性能规范约束,利用消息顺序图对TSRS与外部系统之间的信息交互行为建模,并将系统MSC模型转化为UPPAAL中的时间自动机仿真模型,对系统的功能和性能要求进行形式化验证。验证结果确认了系统的安全性和受限活性,为进一步完善TSRS设计和系统开发提供参考。

Temporary Speed Restriction Server （TSRS） is a key element of the CTCS-3 train control system, and the safety of TSRS directly affects the safe operation of high-speed railway. In order to find the error of system design, and ensure the safety of system, TSRS had to be modeled and verified during its development. The structure of TSRS was analyzed, the system function specification and performance specification were retrieved, and Message Sequence Chart （MSC） was used to model the interaction behavior of TSRS with outer systems, and then the MSC models were translated to the timed automata models. The UPPAAL verification tool was applied to simulate and verify the function and performance requirements of the TSRS, which guarantees the safety and bounded liveness properties of the system model, also it further improves the design and development of the system.