论文部分内容阅读
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)以保证列车在同济南站站台和部分区间线路上行车安全为背景,通过两个实例,分别对静态数据,从数据老化和安全约束条件两个方面进行验证；对动态数据,从动态数据老化、动态数据一致性、安全约束条件三个方面进行验证,说明了采用基于形式化模型方法对数据安全验证是可行的。