CTCS-3级列控系统临时限速建模与验证

Modeling and Verification of Temporary Speed Restriction of CTC-S3 Train Control System

为了满足临时限速系统的实时性要求,采用时间自动机理论,对CTCS-3级列控系统临时限速工作流程分别建立了各设备的时间自动机子模型,进而构成临时限速系统的时间自动机网络模型,并基于临时限速系统技术规范的参数对模型进行赋值;采用BNF语法对临时限速系统待验证的属性进行了形式化描述,并应用UPPAAL验证工具对临时限速模型的安全性和受限活性进行仿真验证.验证结果表明:与现有临时限速系统的时间参数设置相比,修正后的时间参数设置避免了出现系统死锁现象;在不影响安全功能属性和受限活性的基础上,提高了临时限速系统的实时性,可在规范规定时间5 s内做出响应.

In order to meet the real-time performance requirement of a temporary speed restriction （TSR） system of Chinese train control system level 3 （CTCS-3）, timed automata sub-models of each equipment of the train control system were established for the working process of TSR, and a timed automata network model was built through parallel composition of the submodels to valuate the sub- models using the parametric configuration of the specification of CTCS-3. Then, the properties of the TSR system such as safety and bounded liveness were expressed in Backus-Naur form （BNF） and validated through formal verification simulation using the UPPAAL integrated tool. The results show that compared with the parameters defined in the system specifications, the modified time parameters can fix the deadlock problem of the system, and improve the real-time performance of the TSR system on the premise of keeping the system properties such as safety and bounded liveness. The TSR system can respond to inputs within 5 s and meet the system specifications.