高速铁路列控系统运营场景实时性的建模与验证

摘要

The high-speed train control system is a typical distributed real-time system,in which time constraints are mainly focused on the operation scenarios between subsystems.The extension of the temporal logic can not meet all needs of describing the properties of the distributed real-time system.The scenarios of the train control system are often described in terms of the deadline, time-out and wait until and so on.Insufficiency exists in the above formal descriptions and also in verification along with intensification of the complexity of the system.In this paper, the modeling and verification methods suitable for the scenarios of the train control system are introduced.Firstly, HCSP is used to model the distributed real-time system.Secondly,the HCSP models are transformed to the TA models according to transition rules.Finally,automatic verification is accomplished with the checking tool UPPAAL.The effectiveness of the proposed modeling and verification methods are proved through simulation and analysis of RBC handover scenarios.%高速铁路列控系统是一个典型的分布式实时系统,其时间约束主要反映在运营场景中子系统之间的交互过程中.时序逻辑的扩展方法并不能完全满足描述分布式实时系统性质的需要,并且随着系统的复杂性提高,列控系统运营场景中诸如超时、期限、直到…才等形式化描述与验证上存在不足.本文提出一种适合于列控系统场景建模与验证的方法,其核心思想是使用混合通信顺序进程HCSP(Hybrid Communicating Sequential Process)形式化描述分布式实时系统模型,提出转换规则,转换成时间自动机网络模型并进行自动验证.最后通过对典型场景无线闭塞中心RBC(Radio Block Center)切换的相关属性进行建模与验证,分析证明方法的有效性.