论文部分内容阅读
临时限速服务器是CTCS-3级列控系统的重要组成部分,其系统安全性直接影响到高速铁路的运营安全。在TSRS系统研发过程中需对系统进行仿真建模和验证,发现系统设计错误,以保证系统的安全性。分析CTCS-3级列控系统临时限速服务器的组成结构,提取系统功能和性能规范约束,利用消息顺序图对TSRS与外部系统之间的信息交互行为建模,并将系统MSC模型转化为UPPAAL中的时间自动机仿真模型,对系统的功能和性能要求进行形式化验证。验证结果确认了系统的安全性和受限活性,为进一步完善TSRS设计和系统开发提供参考。
Temporary speed limit server is an important part of CTCS-3 train control system, and its system security directly affects the operation safety of high-speed railway. During the development of TSRS system, it is necessary to simulate and verify the system and find that the system design is wrong to ensure system security. The paper analyzes the composition of temporary rate-limiting server in CTCS-3 train control system, extracts the constraints of system functions and performance specifications, models the information interaction between TSRS and external systems by message sequence diagram, and transforms the system MSC model into UPPAAL In the time machine simulation model, the system’s functional and performance requirements for formal verification. The verification results confirmed the safety and limited activity of the system, providing a reference for further improvement of TSRS design and system development.