【作者】 曹源；

【导师】 唐涛； 穆建成；

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

【摘要】 高速铁路列车运行控制系统(简称：列控系统)融入了先进的计算机、通信以及控制技术,极大地提升了系统的效率和安全性。由于系统的硬件集成度不断提高,大量软件参与系统控制,使得系统特性也呈现出结构分布、实时性强、响应快速等多样化的趋势,系统特性的验证也愈加困难,因此需要找到一条更为有效、全面的方法实现列控系统的特性验证,进一步提升系统的性能或完善系统功能。基于严格数学定义的形式化方法,由于其能够精确、清晰地描述系统结构和相关特性,同时能够验证系统的相关特性,近年来在列控系统领域得到迅速发展,并且已经成为描述和验证高速铁路列控系统特性的一种重要方法。论文对列控系统的形式化建模、描述以及验证方法的应用展开了综述。分析了RAISE (Rigorous Approach to Industrial Software Engineering,工业软件工程的严格方法)形式化方法在列控系统中建模与验证的优势,并在此基础上,首次将Timed RAISE(时间化RAISE)引入列控系统验证领域。论文研究了基于域+Timed RAISE的高速铁路列控系统的建模和描述方法。结合高速铁路列控系统的实际特点以及复杂性,提出了一种域方法作为系统描述的切入。域方法的主要思想是将系统划分为规模较小的域模型,根据域的验证结果以及域之间的分解与组合关系,能够最终实现大系统的特性验证。论文详细给出了域的元组、域的组合分解以及域特性的组合分解等相关定义和定理,这些定义与定理也是域方法理论体系的关键组成部分。为实现对域方法的更好说明,对典型的高速铁路列控系统—CTCS-3 (China Train Control System level 3)级列控系统进行了实际的域的划分、域模型的建立、域特性的分析、域特性的组合分解以及子域的划分,实现了对域方法理论体系的有力支撑。论文研究了基于域+Timed RAISE的高速铁路列控系统的验证方法。对高速铁路列控系统常见的运营场景描述相关特性、系统功能以及系统性能等三类重要的域特性进行了详细分析,并给出了三类域特性中的场景交互一致性、安全功能以及实时性的定义和数学描述,并作为系统特性验证的重要依据。论文实现了域模型与Timed RAISE结合,给出了域模型转换为TRSL (Timed RAISE Specification Language)的具体规则,同时也给出了在系统TRSL描述的证明过程中相应的推理规则和证明方法。论文对基于域+Timed RAISE的描述和验证方法的具体应用进行了分析和举例。通过对RBC (Radio Block Center,无线闭塞中心)切换场景的交互一致性验证、等级转换(CTCS-2级至CTCS-3级)场景的实时性验证以及两车区间追踪案例中的安全功能进行了实际的域(子域)的划分、系统模型建立、Timed RAISE具体描述以及验证过程。仅为说明基于域+Timed RAISE方法的正确性,将各验证案例都进行了相应的简化和假设。最终给出了结果：列车通过RBC边界的条件下,车载设备与两个RBC的共同交互并不会带来场景交互一致性错误,即场景中各设备和子系统的交互流程是一致的；列车在等级转换(CTCS-2级至CTCS-3级)场景中,即使GSM-R (GSM for Railway)网络的通信随机延迟给场景的实时性带来了巨大的挑战,但依然能够满足场景的实时性要求；在两车追踪案例中,在给定前车以及外界的边界条件后,CTCS-3级列控系统能够在地面设备、车载设备以及GSM-R无线网络的共同作用下实现列车的安全运行。更多还原

【Abstract】 With the extensive application of advanced computer, communication and control in high-speed railway train control systems, the efficiency and safety have been greatly improved. Because the integration density of hardware enhances and more software participate in control, many new related system characteristics have appeared, like the distributed structure, hard real-time capability, fast response and so on. So the verification of system characteristics becomes more and more difficult, and a solution which can realize the effective and across-the-board verification of high-speed railway train control system should be proposed, and make the system performance and function more improved. The formal methods based on rigorous mathematical definition have developed rapidly in the field of the train control systems, because they can accurately and clearly describe the related characteristics and structure, and verify these characteristics as well, in recent years, they have become an important way to describe and verify the high-speed railway train control system.The formal methods of modeling, description and verification for train control system are discussed and summarized at the first. The advantages of RAISE (Rigorous Approach to Industrial Software Engineering) formal method being applied in the modeling and verification to train control system is analyzed, and on the basis of these analyses, the Timed RAISE is introduced into the verification field of train control system for the first time.The modeling and formal description method which based on the Domain & Timed RAISE for high-speed railway train control system is studied. Combined with the actual characteristics and complexity of high-speed railway train control system, a Domain Method is proposed and this method can be a breakthrough point of system modeling. The main idea of Domain Method is that the system can be divided into small-scale domain models, in accordance with the results of domain’s verification and the relation of combination and decomposition between domains, and then the characteristics verification of whole system can be realized.The relative definitions and theorems about domain tuples, domain combination and domain characteristics are defined in detail, these definitions and theorems are the key components of theory system of Domain Method. In order to give a better illumination to Domain Method, the representative high-speed railway train control system-CTCS-3 (China Train Control System level 3) is divided into domains, and the domain models are built, the domain characteristics are analyzed, the domain characteristics are combined and decomposed and sub-domains are divided in practice, and this practical example mighty supports the theory system of Domain Method.The verification method based on the Domain & Timed RAISE method for high-speed railway train control system is discussed. Three kind common and important domain characteristics of train control system are analyzed in detail:the relative characteristics of scene description, system function and system performance. And accurate mathematical definitions and descriptions of three specific characteristics are given, namely the scene interactive consistency, fundamental safety function and the real-time capability, these definitions and analyses serve as the important base of the verification to system characteristics.The integration of Domain Method and Timed RAISE is achieved, the concrete transformation rules from domain models to TRSL (Timed RAISE Specification Language) are given, and the relevant reasoning rules and specific proving methods in the verification process of TRSL specification are given as well.Some application examples of Domain & Timed RAISE method have been given. The characteristics verification of scene interactive consistency in RBC (Radio Block Center) handover scene, real-time capability in level transition (CTCS-2 to CTCS-3) scene, the safety function during trains pursuit in wayside railway is achieved, and the division of the real domains, the establishment of system models, the formal description and reasoning of Timed RAISE are analyzed and discussed in detail. To merely explain the correctness and validity of Domain & Timed RAISE method, these examples and cases have been simplified and adopt some assumptions. Finally the results are given: on the condition of one train passed the boundary between RBCs, the interactive process between onboard equipment and RBCs will not cause the errors of the scene interactive consistency; in the scene of level transition (CTCS-2 to CTCS-3), even if the uncertainty of GSM-R (GSM for Railway) wireless network is a tremendous challenge to the real-time capability, but this scene still satisfies the real-time requirements; in the case of two trains pursuit, after ascertaining the conditions of head train and the boundary of external environment, CTCS-3 can ensure the safe operation of objected train under the co-action of ground equipments, onboard equipment and GSM-R wireless network.更多还原