车地协同下的联锁子系统HCPN建模与验证

HCPN modeling and verification of interlocking subsystem based on train-ground collaborative control

联锁子系统作为站内行车安全的关键保障,是车地协同下的列车运行控制系统的重要组成部分。传统联锁子系统存在地面集中控制失效风险大、列车自主化程度低等不足,为顺应精简系统结构、降低运营成本和提升列车自主化的列控技术发展趋势,设计一种车地协同下的联锁子系统用于城际铁路。考虑多车间的进路冲突是影响子系统功能实现的关键因素,提出进路预延伸策略以避免列车间的进路冲突。为确保联锁子系统功能安全,采用一种基于层次着色Petri网(HCPN)的系统功能建模与验证方法。通过对联锁子系统的主要功能实现过程—进路建立过程进行分析,提取子系统的功能需求,以此建立顶层需求模型。为缩小底层实现与顶层需求之间的差距,建立基于数据及行为低抽象度表达的模块层模型,并在其中引入死锁控制策略实现对系统功能逻辑的完整表达。以冲突进路建立场景为模型的输入参数,执行验证过程,通过对模型标准状态空间性能分析,实现对模型正确性的检验。在此基础上,采用分支时序逻辑ASK-CTL公式与状态空间搜索算法相结合的验证方法,完成对子系统功能安全性的检验。研究结果表明:模型的行为特性同子系统预期相一致,能够正确表达系统的行为。所设计子系统满足功能安全需求,可为底层实现提供依据。

As a key to guaranteeing the train in the station,the interlocking subsystem is an important component of the train control system in the train-ground collaborative way.The traditional centralized interlocking subsystem has the disadvantages,such as the high risk of centralized control failure and the low degree of train autonomy.For the intercity railway,an interlocking subsystem based on train-ground collaborative control was designed in accordance with the development trend of train control technology of simplifying system structure reducing operation cost and improving train autonomy.A route pre-extension strategy was proposed to solve the conflict of route among multiple trains,which was the key factor to affect the realization of subsystem functions.Secondly,based on Hierarchical Colored Petri Nets(HCPN),a method of system function modeling and verification was applied in order to ensure the functional safety of the subsystem.In the process of modeling,according to analyzing the route establishment process which was the main function realization process of this interlocking subsystem,the functional requirements of the subsystem are extracted out and the top-level requirements model was established.At the same time,for closing the big gap between the subsystem functional requirements and the underlying implementation,a module layer model based on low abstraction expression of data and behavior was established,in which a deadlock control strategy was introduced to realize the complete expression of subsystem functional logic.Finally,with resistant departure routes being regarded as input parameters of the model,its functional safety was checked by using the verification method combining ASK-CTL formula of computing tree logic and state-space search algorithm.With the checking as a basis,the subsystem correctness was verified by analyzing the performance of the standard state space.The verification results show that the behavior characteristics of the subsystem and the model are consistent,consequently,the former can be correctly expressed by the model.Meanwhile,the subsystem satisfies the expected functional safety characteristics,which can provide the foundation for the underlying implementation.