【作者】 吕继东；

【导师】 唐涛；

【作者基本信息】 北京交通大学 ， 交通信息工程及控制， 2011， 博士

【摘要】 列车运行控制系统(简称“列控系统”)是将先进的控制技术、通信技术、计算机技术与铁路信号技术融为一体,保证轨道交通安全、正点、高密度运行的自动化系统。随着计算机在列控系统中的广泛应用,硬件和软件规模不断扩大,系统的复杂性有了很大的提高,呈现出复杂的系统特性(并发性、实时性和混合属性等等)。作为一个复杂安全苛求系统,列控系统中任何故障都有可能造成重大的人身伤亡和财产损失,如何保证系统的正确性,寻找一套全面的、有效的建模与验证方法是非常必要的。相比仿真和测试技术,基于严格数学定义的形式化方法不仅能精确、清晰地描述系统结构和相关特性,而且能对特性进行验证,近年来已经成为列控系统建模和验证的一种重要理论方法。论文引入系统层次化建模概念,利用面向对象的建模思想和基于场景的系统设计理念,提出了一套包含系统层、场景层、组件层和功能层的列控系统层次化模型。在此基础上,提出了一个集成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切换场景和行车许可场景的分层形式化建模与验证分析,验证了列控系统的实时性和混合属性,最大限度的避免了系统设计上的缺陷和错误,为进一步解决列控系统建模与验证的关键理论问题,保障列控系统安全可靠的应用和运营提供重要的理论基础。更多还原

【Abstract】 The Train Control System is an automatic system which is integrated of advanced control technology, advanced communication technology, advanced computer technology and railway signal technology. It plays an important role in assuring safety and improving efficiency in railway. The increasing usage of computer technology has led to the increasing complexity in the train control system with large scale of software and hardware, which has exhibited highly distributed, real-time, safety and hybrid properties. As a complex safety-critical system, any fault in train control system can lead to huge human injury or wealth losing. It is necessary to find a more effective and across-the-aboard modeling and verification methodology to guarantee the correctness of train control system. As is compared to simulation technology and testing technology, formal methods based on rigorous mathematics definition have become an important modeling and verification theory in the field of train control systems due to its accurate and clear description of system architecture and related characteristics.A hierarchical model of train control system including system layer, scenario layer, component layer and function layer is proposed firstly by introducing hierarchical modeling conception, using object-oriented methodology and scenario-based design methodology. Based on the hierarchical model, a hierarchical formal modeling and verification framework which is integrated of HCSP, CHARON and TL is proposed. It is not only suitable for verifying all the characteristics of train control system, but also improves the modeling efficiency due to its hierarchical and reused characteristics.The real-time properties of operation scenario in train control system are deeply researched. Six time constraints stated in terms recursion, delay, wait until, time-out, deadline and time interrupt are proposed. Some transition rules are introduced for transiting the HCSP subset models to TA network models. The real-time properties of operation scenario are described using TCTL, and finally a procedure is given for verification based on the simulation.The hybrid properties of operation scenario in train control system are deeply researched. It is pointed that the traditional formal methods of hybrid system are not well in describing communication behaviors which occur in the interactive process of subsystems. To overcome this problem, we introduce a formal modeling and verification method by extending the HCSP syntax and semantics. We transit the HCSP models to HA models by introducing some transition rules based on some assumptions. The hybrid properties of operation scenarios are described using ACTL, and finally a procedure is given for verification based on the simulation.Finally, two typical cases of operation scenario which are RBC handover scenario and movement authority scenario are chosen according to the general technical programming of CTCS level 3 train control system in railways for passengers. Based on the two hierarchical formal modeling and verification models, the real-time and hybrid properties of CTCS-3 train control system are separated verified. As a result, it avoids the maximum fault and error in the system design. It is considered that the method is powerful for solving the key problems in modeling and verification train control system. It is of great significance for ensuring the safety and reliability in train control system.更多还原