基于时间自动机的CTCs-3级列控系统建模方法与验证研究

摘要

CTCS-3级列控系统的实时性依据技术规范而实现。如果技术规范存在缺陷，则会严重危及行车安全或影响行车效率。因此，有必要对列控系统的实时性进行分析研究，以验证技术规范的正确性。
　　目前，验证系统实时性的途径有仿真、测试、形式化方法三种。仿真和测试存在固有的缺陷，形式化方法可以最大限度地分析验证系统。通过比较多种验证系统实时性的形式化方法得出:时间自动机理论更为适合验证CTCS-3级列控系统的实时性。
　　本文提出一种基于时间自动机的列控系统建模与验证方法。科学地阐述时间自动机模型与列控系统的一致性、所建模型的正确性、模型验证结果的可信性等问题，创造性地提出对列控系统进行VV&A分析的原则和过程，建立了基于时间自动机的列控系统建模与验证框架，并说明了该建模与验证方法对CTCS-3级列控系统各个运营场景的普遍通用性。其建模与验证的一般流程为:用时间自动机语言规约列控系统的行为和动作，得出列控系统的时间自动机模型，然后用UPPAAL验证工具对系统模型所反映的特性进行验证。
　　以CTCS-3级列控系统临时限速和等级转换运营场景为例，说明了该建模与验证方法的有效性。利用时间自动机理论，分别建立临时限速工作流程、等级转换过程的时间自动机网络模型。同时，应用UPPAAL验证工具对临时限速系统、等级转换过程的安全性和受限活性进行仿真分析。找到了临时限速技术规范中不能达到实时性要求的时间参数设置，并给出了修正值。此外，等级转换模型成功验证了等级转换过程的安全性。验证结果表明:该建模与验证方法可有效研究CTCS-3级列控系统临时限速和等级转换的实时性。