基于UML顺序图与UPPAAL的列车追踪模块建模研究

摘要：区域控制器(zone controller, ZC)是一个实时复杂系统， 它要求过程控制的准确性。 列车追踪场景是城市轨道交通(communication based train control, CBTC)系统中ZC的一个重要功能。 在对系统进行深层次的开发设计过程中需要对系统进行建模、 仿真和验证， 发现系统设计缺陷， 以保证系统的安全性。 通过分析ZC系统结构及列车追踪分界点处理过程， 给出满足系统安全性的功能要求和性能要求， 并采用统一建模语言(unified modeling language, UML)与时间自动机相结合的方式建立列车追踪场景中列车筛选和列车追踪分界点的时间自动机网络模型。 同时， 应用UPPAAL验证工具对系统进行仿真模拟， 验证了系统的功能和性能要求。 结果表明， 列车追踪分界点功能满足系统安全性和受限活性的规范要求。 因此， 此种建模方法是可行的， 可以将其应用于列控系统其他场景的建模与验证过程中。
Abstract： The zone control subsystem is a real-time control system, which requests the correctness of the control process. Train tracing scene is an important function of the zone controller (ZC) in the communication based train control (CBTC) system. In the process of deep development and design, to ensure the safety of the system, the system needs to be modeled, simulated and verified to discover the system design flaws. Unified modeling language (UML) is combined with timed automata, and timed automata network models of train-filter and train tracing demarcation-point are established. At the same time, the verification tool of UPPAAL is applied to simulate the system, and verify the requirements of performance and function of system. The results show that the function of train tracing demaraction-point meets the requirements of system safety and limited activity. Therefore, the method is feasible and can be applied to the modeling and verification of other scenes of train control system.