列车运行控制系统分层形式化建模与验证分析

摘要

列车运行控制系统(简称“列控系统”)是将先进的控制技术、通信技术、计算机技术与铁路信号技术融为一体,保证轨道交通安全、正点、高密度运行的自动化系统。随着计算机在列控系统中的广泛应用,硬件和软件规模不断扩大,系统的复杂性有了很大的提高,呈现出复杂的系统特性(并发性、实时性和混合属性等等)。作为一个复杂安全苛求系统,列控系统中任何故障都有可能造成重大的人身伤亡和财产损失,如何保证系统的正确性,寻找一套全面的、有效的建模与验证方法是非常必要的。相比仿真和测试技术,基于严格数学定义的形式化方法不仅能精确、清晰地描述系统结构和相关特性,而且能对特性进行验证,近年来已经成为列控系统建模和验证的一种重要理论方法。
　　 论文引入系统层次化建模概念,利用面向对象的建模思想和基于场景的系统设计理念,提出了一套包含系统层、场景层、组件层和功能层的列控系统层次化模型。在此基础上,提出了一个集成HCSP(Hybrid Communication Sequential Process)、CHARON和TL(Temporal Logic)的列控系统分层形式化建模与验证框架。该框架不仅适合列控系统各种特性的验证分析,而且建立的模型具有可继承性、重用性,在保证系统模型一致性的基础上,提高了建模的效率。
　　 论文深入分析了列控系统运营场景实时性的验证问题,提出了六种适合于列控系统运营场景描述的时间约束类型:周期性、延迟、时间等待、超时、截止期限和时间中断；提出了HCSP的子集模型到时间自动机网络模型的转换规则；给出了运营场景实时性约束的TCTL(Timed Computation Tree Logic)描述；实现了运营场景中相关实时属性的验证流程。
　　 论文深入研究了列控系统运营场景的混合属性验证问题,指出了传统的混杂系统建模与验证方法在刻画列控系统场景中通信行为上存在的不足。并根据现有HCSP方法的不足,提出了HCSP的假设条件；结合混合自动机的语义,提出了HCSP模型到混合自动机模型的转换规则；给出了运营场景中混合属性的ACTL(Action Computation Tree Logic)表达；实现了运营场景中相关混合属性的验证流程。
　　 论文最后选取了CTCS-3级列控系统总体技术方案中两个典型的运营场景(RBC(Radio Block Center)切换场景和行车许可场景)作为案例来分析。通过对RBC切换场景和行车许可场景的分层形式化建模与验证分析,验证了列控系统的实时性和混合属性,最大限度的避免了系统设计上的缺陷和错误,为进一步解决列控系统建模与验证的关键理论问题,保障列控系统安全可靠的应用和运营提供重要的理论基础。