高速铁路CTC分界口临时限速系统建模与验证

临时限速是高速铁路列控系统的重要组部分,CTC行车调度台分界口处的临时限迷信息交互频繁,对实时性的要求也更苛刻.为满足其实时性要求,采用时间自动机理论,结合分界口处临时限速相邻设备间的交互过程,分别建立各设备的时间自动机模型,通过时间自动机的积构建整个交互系统的网络模型,并利用UPPAAL验证工具对模型的功能和性能属性进行形式化验证.验证结果确认了交互过程中系统的安全性和受限活性.

Modeling and verification of Temporary Speed Restriction System in boundary area of CTC

Temporary speed restriction（TSR） was an important part of the Train Control System in the passenger special line,the process of information interaction was frequent in the boundary area of CTC dispatching platform,and the requirement of the real-time nature was much higher.To satisfy the real-time requirements,timed automata sub-models of each equipment were established for the working process of TSR in the boundary area of CTC,and the overall timed automata network model was built through parallel composition of the sub-models.Then,the function and performance properties of the System were validated through formal verification simulation using the UPPAAL tool,The verification results confirmed the safety and bounded liveness properties of TSR System in the boundary area of CTC.