基于混成自动机的城市轨道交通ZC子系统建模与验证方法

Modeling and Verification Method of ZC Subsystem in Urban Rail Transit Based on Hybrid Automata

结合城市轨道交通列车控制系统区域控制器(ZC)子系统的混成特性,采用扩展的统一建模语言(UML)建立ZC子系统的UML顺序图;采用模型转换方法,提出从源模型到目标模型转换的定义和规则,将ZC子系统的UML顺序图转换为形式化的线性混成自动机模型,用于ZC子系统功能的安全验证。以北京地铁亦庄线ZC边界切换控制功能场景为例,建立该场景的UML顺序图;将其对应车地通信的5个阶段细分为5个组合片段;根据模型转换定义及规则,将各组合片段转换为线性混成自动机,进一步将不同组合片段的线性混成自动机合成完整的目标线性混成自动机;根据建立的线性混成自动机模型,采用验证工具BACH对该场景的7条功能性质和4条安全性质进行验证。结果表明:ZC边界切换控制功能满足设计需求,列车能够安全通过地面区域边界点,没有超速情况且能够在接管ZC管辖范围内安全停车。表明所提出的建模和验证方法是可行的,弥补了对具有混成特性列车控制系统既有验证方法的不足。

In combination with the hybrid characteristics of Zone Controller（ZC）subsystem in the train control system for urban rail transit,the UML sequence diagram of ZC subsystem was established by extended Unified Modeling Language（UML）.According to model transformation method,the definition and rules for transforming from the source model to the target model were given.The UML sequence diagram of ZC was converted into formalized linear hybrid automata model for the safety verification of ZC functions.Based on the scenario of ZC boundary handoff control function in Yizhuang Line of Beijing Metro,the UML sequence diagram of the scenario was established.The five stages corresponding to train-ground communication were subdivided into five combination fragments.According to model transformation definition and rules,each combination fragment was converted into linear hybrid automata,and then the linear hybrid automata of different combination fragments were further combined into complete target linear hybrid automata.According to the established model of linear hybrid automata,the seven functional properties and four safety properties of the scenario were verified by the verification tool BACH.The results show that ZC boundary handoff control functions meet the design requirements.The train can safely pass the boundary point of ground region without exceeding speed limit and can be safely stopped within the take-over range of ZC.The feasibility of the proposed modeling and verification method has been proved,and the deficiency in the existing verification method for train control system with hybrid feature is made up.