基于Timed-UML顺序图的RBC交接形式化建模与分析

在CTCS-3级列控系统中,采用RBC技术将线路划分成多个管辖区段。当列车行驶并跨越相邻RBC交界区域时,控制权将会移交至前方相邻RBC,整个过程称为RBC交接。在运行中,RBC交接过程能否实时安全可靠地执行,直接影响着列车的行车效率和乘客的生命安全。采用一种基于添加实时约束的UML顺序图与时间自动机结合的模型来建立RBC交接场景。以双车载电台的RBC切换策略出发,建立切换的Timed-UML顺序图模型,然后按照UML-TA转换规则,建立得到完整的时间自动机网络模型。并利用UPPAAL验证工具对RBC交接模型进行形式化建模及分析,对模型的死锁和功能实现做了验证,从而达到对CTCS-3级RBC子系统的实时性以及设计规范合理性的验证目的。

Formal Modeling and Analysis of RBC Handover Based on Timed UML Sequence Diagram

In the CTCS-3 level train control system,a line is divided into several RBC control sections.When the train runs through an adjacent RBC region,the control of the train will be handed over to the region,which is called RBC handover. In the operation of the train,safe and reliable RBC handover is the key to the operation efficiency and safety of passengers. In this paper,a model based on the combination of the UML sequence diagram with the time automaton with real-time constraints is used to establish RBC handover scenario. Based on RBC switching strategy of dual onboard radio station,the timed-UML sequence diagram model is established,and then the complete time automaton network model is established according to the UML-TA conversion rule. The UPPAAL verification tool is used to model and analyze RBC handover. The deadlock and the function realization of RBC handover model are verified to confirm the real-time performance and the rationality of the design specifications for CTCS-3 level control system.