基于MSC与UPPAAL的区域控制器切换场景建模与验证

区域控制器(Zone Controller,ZC)边界切换场景是城市轨道交通列车控制系统的重要场景,切换过程中移交ZC、接管ZC和车载子系统之间要进行频繁的信息交互,因而对其安全性和实时性有更严苛的要求。根据ZC子系统特点,将MSC半形式化方法作为切入点,结合时间自动机理论,建立ZC切换场景的MSC模型和时间自动机网络模型,用于ZC切换场景功能和受限活性的安全验证。结果表明:ZC边界切换控制功能满足系统安全性和受限活性的规范要求。因此此种建模验证方法是可行的,可以将其应用于列控系统其他场景的建模与验证过程中。

Modeling and Verification of Switch Scene of Zone Controller Based on MSC and UPPAAL

The border switch scene of zone controller( ZC) is an important scene of Urban Rail Transit Train Control System. During the switch process,the handover ZC,the takeover ZC and the vehicle interchange information frequently,and the requirements for its security and real-time performances are more stringent. In this paper,a combination of the MSC semi-formalization method is taken as the entry point and the time automaton theory is used to establish the MSC model and the time automaton network model of ZC switch scene to fulfill the safety verification of ZC switch scene function and limited activity.The results show that the ZC border switch control function meets the requirements of the system security and limited activity. Therefore,this modeling and verification method is applicable to modeling and verification of other scenes of the train control system.