本质特征驱动的高铁列控系统安全逻辑建模理论与方法

High-speed rail is a core part of the pillar industries of the national economy. Train control system is the equipment to protect the rail traffic safety,shouldering a huge social responsibility.Its safety mechanism is very complex;the operating environment is dynamic,heterogeneous and continuous evolution.Currently,there is no feasible modeling method,hence,design flaws are easily formed,the system safety is facing enormous challenges. Considering the essential features of the train control safety logic, this project proposes modeling theory and methods for train control system. Specially including: (1) Revealing the commonalities and variability of the control law by perceiving and abstracting the control processes of train operation, proposes the essential features of train control safety logic;(2) Extending the preliminary research results based on the essential characteristics,to investigate a formal mathematical specification theory and representation methods of the safety logic;(3)For core safety-critical functions, presents features-oriented modeling methods of train control safety logic, to make the model closer to the physical objects and behavioral processes.(4) Finally, the completeness problem of safety verification will be solved, and the verification algorithm is established by theorem proving of the safety properties, and a runtime safety logic verification methods will be proposed for high-speed rail train control system. The project has far-reaching scientific significance and broad application prospects, will effectively address the design deficiencies, and provide technical support to the efficient development and system safety of train control systems for high-speed railway.

高速铁路是国民经济支柱产业轨道交通的核心组成部分。列控系统是保障行车安全的关键技术装备，肩负着巨大社会责任，其安全机理异常复杂，运行环境动态、异构、持续演化，目前尚无成熟建模方法，极易造成设计缺陷，系统安全面临巨大挑战。本项目面向列控本质特征，研究列控安全逻辑建模理论与方法，具体包括:(1)对列车运行控制过程进行感知和抽象，揭示控制规律的共性和变化性，提出列控安全逻辑的本质特征；(2)对前期研究成果进行扩展，研究安全逻辑的数学规约理论和形式化表示方法；(3)围绕本质特征研究核心关键功能安全逻辑数学模型，使模型最大限度地贴近物理对象和行为过程；(4)解决安全性验证的逻辑完备性问题，通过对安全属性的定理证明建立验证算法，提出高铁列控系统安全逻辑运行时验证方法。 本项目研究具有深远的科学意义和广阔的应用前景，将有效解决列控系统的设计型缺陷问题，为我国高铁列控系统的高效开发与安全运行提供技术支撑。

列控系统是保证铁路运输安全、提高运输效率的核心技术装备，是铁路运输的“大脑和神经中枢”。我国高速铁路运营里程已接近3万公里，居世界第一位。列控系统直接关系到广大乘客的人身安全，现阶段的高速铁路列控系统规模越来越庞大、功能不断扩展延伸，具有并发、实时、混成等复杂特征。常规的规约理论、建模、验证方法由于没有考虑复杂的列控特征，往往无法直接应用于列控系统。如何面向复杂开放式列车运行控制过程，研究符合列控本质特征的形式规约理论，建立直观的、揭示列控安全逻辑本质特征的系统模型，对高速列车运行的安全性进行验证，为我国列控系统高效开发与安全运行提供技术支撑，具有重要的理论意义和实用价值。. 本项目围绕列控系统安全逻辑的形式规约、建模及安全性验证三个科学问题，研究本质特征驱动的高铁列控系统模型构建理论与方法。具体研究目标是提出一套本质特征驱动的高铁列控系统安全逻辑建模理论与方法，以支持我国列控系统的设计、开发、分析验证与运行安全，在理论和方法上取得原创性成果和关键技术突破，有效解决现阶段系统存在设计型缺陷的问题。. 四年来，本项目按计划顺利执行，超额完成了计划研究任务和预期指标。已发表学术论文19篇，其中SCI收录7篇，EI收录17篇。申请发明专利3项，其中已授权1项；申请软著3项。培养博士生5名，硕士生22名。面向高铁列控系统，我们分析了列控系统的本质特征，提出了一种新的列控系统安全逻辑框架。提出了一套安全逻辑的规约理论和表示方法，给出了一种统一列控数据模型和列控系统混成建模方法；提出了一种基于PST理论的列控安全逻辑建模方法，建立了基于SCADE的进路控制逻辑模型、列车管理和超速防护控制逻辑模型；提出了基于图论的列控数据验证方法、混成运行时验证方法、以及基于PST的列控安全性验证方法。取得了一系列创新性研究成果，并对这些成果进行了充分的实验验证，部分理论研究成果在我国新型列控系统开发中得到了示范应用。