【作者】 黄友能；

【导师】 唐涛；

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

【摘要】 CBTC系统作为保证行车安全的列车自动控制系统,具有基于计算机控制、移动闭塞追踪、闭环控制等优点。相比传统的固定闭塞列车自动控制系统：CBTC系统通过不同种类的数据来实现对系统真实环境的描述和系统功能的驱动,数据安全是CBTC系统安全的一个重要组成环节,但保证数据安全是轨道交通安全生产的突出薄弱环节。因此,开展CBTC系统数据安全的研究具有重要意义。本文以我国自主研制的CBTC系统为研究对象,围绕如何保证CBTC系统数据安全,建立了基于数据驱动的CBTC系统模型,总结了CBTC系统数据描述对象多、数据之间存在安全约束关系、系统具有数据老化的特点,提出了通过保证数据之间正确的安全约束关系来确保数据正确,从而达到数据安全的目的。然后,在分析了数据错误类型的基础上,明确了从数据处理和数据验证方法上开展研究的必要性。本文主要成果和创新点如下：(1)本文针对静态数据描述对象多的特点,给出了数据结构化描述方法；针对静态数据之间存在的拓扑规则、属性规则,提出了通过SAT方法对静态数据进行了处理,解决了静态数据虚假数据错误及值错误的问题,同时,结合列控系统VOBC子系统和ZC子系统分别在计算位置和移动授权时,对线路拓扑的需求,给出了系统拓扑描述方法以及有约束条件的路径搜索算法,解决拓扑逻辑错误的问题。(2)本文分析了列车追踪运行模型,提取列车位置和移动授权两个动态数据进行处理,研究了列车安全位置处理方法,同时,在分析了移动授权生成模型的基础上,提出了移动授权性能和功能安全约束条件,并采用LTL对安全约束条件进行了处理。(3)针对静态数据中存在的条件关系,提出了采用基于CSP模型的数据安全验证方法,以UML为源模型,通过LTS语义转换以及模型转换规则,将UML建立的时序模型转换为CSP模型进行验证,并通过实例说明了模型转换方法的可行性。(4)针对动态数据中存在的依赖关系和数据老化特点,提出了基于TA模型的数据安全验证方法,以UML为源模型,进行了时间上的扩展,并给出模型转换规则,将UML建立的时序模型转换为TA模型进行验证,解决了动态数据存在的一致性问题和数据在应用过程中出现的组合错误问题,并通过实例说明模型转换方法的可行性。(5)以保证列车在同济南站站台和部分区间线路上行车安全为背景,通过两个实例,分别对静态数据,从数据老化和安全约束条件两个方面进行验证；对动态数据,从动态数据老化、动态数据一致性、安全约束条件三个方面进行验证,说明了采用基于形式化模型方法对数据安全验证是可行的。更多还原

【Abstract】 As a kind of automatic train control system used for safety assurance, CBTC systems has advantages of computer-based control, moving block tracking and closed loop control, etc. Compared with the traditional fixed block train automatic control system, CBTC systems describe the real system environment and drive the system function with different kinds of data. Data safety is an important aspect of CBTC system, but how to ensure data safety is a weak link of rail transit. The research of data safety in CBTC systems is of great significance. Based on the independently developed CBTC system of China, this thesis focuses on how to ensure data safety in CBTC systems. The author establishes the data-driven model and summarizes the characters of CBTC system, which includes large number of CBTC system data objects, safety constraint relationship among the data and data aging problem, etc. According to these characters, we propose a method to ensure the correctness of the restricted safety relationships among data to ensure the data safety. Then, on the basis of analysis on data error type, we study the data processing and data verification. The main achievements and innovations are shown as follows,(1) According to the large number of static data objects, this thesis proposes a method to describe structured data. Among static data for topology rules, attribute rules proposed by SAT methods for static data are processed to solve the problem of the static data errors and false data values. At the same time, when VOBC subsystem and ZC subsystem calculate the position and MA respectively, this thesis present topology description method for the system and constraint conditions of path search algorithm, to solve the problem of topological logic errors.(2) In this thesis, the operating train model is analyzed to extract the train position and mobile authorized data to study the treatment of safe location. At the same time, on the basis of the analysis on the model, this thesis introduces the performance and constraints of functional safety mobile authorization and deals with safety constraints by the LTL method.(3) For the relationships among the static data, this thesis proposes a data safety verification method which is based on CSP model. The proposed model is based on UML source model and it can transform time-series UML model into CSP model through the LTS model semantic conversion and transformation rules. Besides, an example is given to illustrate the feasibility of the model transformation method.(4) For the dynamic data dependencies that exist in the aging characteristics, this thesis presents a data safety verification method which is based on TA models. According to model transformation rules, this thesis transforms UML timing model into TA model. It solves the consistency problems of the dynamic data and the application of composite error problem when using of the data. One example is given to illustrate the feasibility of the model transformation method.(5) To ensure the safety of train, this thesis chooses platform of Tongjinan station and part of range line to do static and dynamic data safety validation test. This thesis uses aging data and safety constraints to verify the static data and uses data consistency, data aging and data safety constraints to verify the dynamic data. The result illustrates the feasibility of formal model-based approach on data safety verification.更多还原