基于Event-B的联锁进路控制建模验证方法研究

计算机联锁系统具有典型的安全苛求特性.传统的联锁软件开发方法难以完整准确地定义需求,单纯依靠测试也无法发现软件中的所有错误,使软件在功能完整性和安全性方面难以得到保证.本文利用形式化Event-B方法和相关工具对联锁系统的核心功能-进路控制的相关功能需求和安全需求进行了建模、精化和验证,对开发高安全苛求和高可靠性的联锁软件提供了新的方法借鉴.     

属性驱动的列车控制系统需求建模与验证

形式化语言越来越多地用来描述列车控制系统需求规范,其精确的语法和语义一方面有助于创建精确的需求模型、消除理解差异,另一方面也为进一步分析验证提供了基础.通过提出一种基于属性的需求分析方法,利用具体的形式化技术来分析需求.首先将由自然语言描述的需求规范转换为属性描述语言(PSL)形式化规范,并通过仿真和博弈分别进行语义检查和可实现性验证,最后通过断言来检验形式化语言所刻画的系统的精确性和完整性.该方法从自然语言形式的需求约束中直接提取相关需求规范,构造形式化模型并进行验证,为需求的早期确认提供了一种新的实用途径.并以CTCS-3级列控系统RBC切换场景为例,说明该方法的有效性.     

基于Prover的联锁软件形式化验证过程研究

计算机联锁系统是铁路信号控制系统的核心设备,是有着苛刻安全要求的复杂控制系统。本文采用Prover形式化开发工具对联锁软件安全需求进行形式化验证。通过模型检验的形式化验证方法,遍历系统输入变量的所有状态空间.验证联锁特定应用满足系统安全需求,确保系统的安全性得以正确实现。在保证系统安全性的基础上,以全状态空间查找反例的检验方法进一步提升产品的质量。     

一种基于场景模型的安全性分析算法研究

为了确保安全苛求系统的安全性,其开发过程中必须使用安全性分析技术.传统的安全性分析方法需要花费大量的时间和精力,分析的完整性和一致性难以保障,分析结果易于出错.本文提出一种基于场景模型的安全性分析算法,该算法从基于UML时序图的需求描述出发,生成系统的形式化模型,通过故障自动注入与形式化模型扩展,采用扩展的启发式广义büchi自动机判空检测算法自动验证与分析系统的安全性.通过铁路车站联锁系统中基本进路建立的安全性分析实例,验证了该方法的正确性与实际可行性.与已有的安全性分析方法相比,本文提出的方法从效率和安全质量方面改善了安全苛求软件的设计与开发,为安全苛求系统的安全性保障与安全评估提供了有力的技术支撑.     

联锁系统UML模型的建立与形式化验证

针对目前计算机联锁系统建模与验证难度较大的问题,提出一种UML(Unified Modeling Language)与NuSMV(New Symbolic Model Verifier)相结合的计算机联锁模型形式化检验方法。以一个标准站场中的一条接车进路建立过程为例,对联锁系统需求进行分析并通过UML建立相应的模型,再列出它与NuSMV之间的映射关系并实现将UML模型自动转换为NuSMV形式化模型,最后完成对计算机联锁系统的验证,检测其需求中可能存在的漏洞。该方法能够降低对计算机联锁系统形式化建模与验证的难度与减少人工建模时可能出现的错误,为计算机联锁系统形式化模型的建立与验证提供一种新思路。     

CTCS-3级列控系统规范的建模与形式化验证方法研究

CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节。然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验证显得十分必要。本文提出CTCS-3级列控系统规范建模与形式化验证方法,此方法的特点是能够在系统规范、模型、验证工具以及验证结果之间建立一条跟踪链,从而始终保证系统规范、模型及程序代码之间的一致性。结合笔者运用此方法对CTCS-3级列控系统规范建模与形式化验证的实践,证明这种方法是可行的、高效的。     

形式化方法应用于计算机联锁软件的安全验证研究

铁路信号系统中的联锁系统对安全性要求极高，仅通过普通的功能测试无法保障其安全性。采用形式化验证的方式可以验证联锁系统的应用逻辑与安全需求的一致性。将通用安全需求结合具体的站场图进行实例化，得到具体的安全需求后输入带归纳功能的布尔可满足问题（SAT）约束求解器进行验证，通过覆盖所有的实例、所有周期以及每个周期所有的状态空间，保证了验证方法的完备性。     

面向形式化验证的联锁翻译器软件设计

根据联锁系统的形式化验证系统需求,设计一种联锁数据翻译器软件的总体方案,实现站点接口文件、TLE文件和布尔逻辑文件等文件的翻译转换,生成形式化验证所需要的LCF文件.最后详细说明翻译器软件基于函数式语言OCaml的代码实现.     

角色自律分散系统的RN-C形式化描述方法

旨在为角色自律分散系统的建模提供一种形式化方法,为形式化验证奠定基础.角色随时空变化的动态表达取决于系统的自律度和环境条件.在对几类系统自律性的度量指标分析比较的基础上,从内部视点和外部视点2个角度,以及行为层、协调层和规范层3个层次,定义了角色自律度矩阵;提出了角色规范-条件(RN-C)形式化描述方案,包括角色、角色空间、规范、角色转换、行为条件等基本要素.应用RN-C方案,建立了角色行为状态的自激状态声明和受控状态声明的形式化描述;给出了角色域与数据域双重驱动体系结构中的行为原语描述,包括操作行为原语、请求行为原语、改变行为状态原语、角色仲裁行为原语;实现了角色自律分散系统行为的形式化描述.指出基于分层有限自动机的角色演化建模,环境依存度与规范-条件的映射关系等是下一步研究的重点.     

铁路联锁与调度集中标准接口规范缺陷分析及升级研究

深入研究当前联锁系统与调度集中系统的标准接口规范协议,分析得出既有协议不符合国标的缺陷点,结合现场双方接口实施时发现的不合理之处,提出在RSSP-I安全通信协议的框架下,定义新的联锁与调度集中接口规范,实现符合安全标准的接口通信,确保数据报文的安全传输;对原有协议进行分析,按照业务数据帧细分归类,构建联锁端和调度集中端的基础通信协议蓝本,并进行试验验证。经过测试,确定基于RSSP-I框架构建通信协议可以适用于双方数据交互,能够解决当前接口规范的缺陷,满足现场的应用数据传输,符合国标和欧标的安全通信要求。     

基于VxWorks的计算机联锁控制系统软件研究

铁路车站信号计算机联锁控制系统是实时、多任务、安全苛求的计算机控制系统.分析DOS和Windows环境联锁控制软件设计存在的问题,结合VxWorks操作系统的特点,研究基于VxWorks实现联锁控制的可行性,在此基础上提出了一种VxWorks环境下设计联锁软件的方法,并进行了详细的系统设计.针对一个实际站场的编码测试结果表明,在VxWorks环境下更易于满足联锁软件对实时性、多任务调度的设计要求,并有利于提高系统的安全性.     

轨道交通信号系统计算机联锁采集方式的分析

对国内轨道交通信号系统计算机联锁采集现状进行了简要分析,并对计算机联锁双断采集和前后接点采集两种方式进行比较分析,从安全性与可用性两个方面比较了故障情况下两种采集方式的优缺点,对比的结果可作为设计及选择联锁采集方式的参考。     

计算机联锁系统在城市轨道交通应用中的新变化

根据城市轨道交通信号系统的特点,分析了城市轨道交通计算机联锁系统相对于国铁计算机联锁系统的一些新需求;介绍了计算机联锁系统因之增加的与外围设备的各种安全接口;详细分析了城市轨道交通的这些新需求、与外围设备的各种新接口对于联锁逻辑判断所产生的一些变化和影响。     

信号联锁关系中的侧防研究

LZB700连续式信号控制系统联锁关系在描述和试验上,与国产信号系统有所不同。针对西门子LZB700连续式信号控制系统联锁关系中“侧防”概念进行解析,分析了这个概念与国产信号系统的联锁关系的关联与区别,并对试验步骤和方法进行了说明。     

基于时间自动机的CBI道岔转换时间建模与验证

针对CBTC计算机联锁安全性十分重要的问题，介绍时间自动机理论，分析CBTC计算机联锁系统的结构和与传统联锁系统的区别，以CBTC联锁系统的道岔转换功能为例，采用UPPAAL建立了道岔转换模型，分析模型的安全需求。表明了在联锁系统开发过程中采用基于时间自动机建模与验证的方法的可行性和有效性。     

基于站场图形网络的计算机联锁软件在高速铁路的应用研究

为适应高速铁路列控系统接口需求,计算机联锁系统接入信号安全数据网[1]的同时,应用软件需要新增进路模块来实现接口的应用信息交互。进路模块利用原有联锁软件网络化结构的选路原理,实现了进路信息存储;利用进路中道岔的大号码特征,实现符合黄闪黄条件信号显示自动计算。软件采用模块化设计的同时,对软件需求、设计、结构、安全性进行全面分析,确保联锁子系统软件的兼容性和可持续开发性。基于升级的计算机联锁软件不仅满足高速铁路列车控制系统的需求,也提高了原有软件的安全性和可靠性。     

计算机联锁软件的黑盒测试过程分析与实现

结合计算机联锁系统的硬件和联锁软件的特征,介绍了软件的测试目的、步骤、黑盒测试中等价类划分法以及安全测试常用的故障树分析法。基于由测试软件、联锁软件和车站信号设备仿真系统组成的测试平台的联锁软件测试,在联锁软件黑盒测试覆盖率准则的基础上,举例介绍了用等价类划分法编写测试用例和用故障树分析法编写安全性测试用例以及测试流程,并用python伪代码实现了“进路正常选出”的测试用例。通过上面的方法来体现黑盒测试在计算机联锁软件逻辑运算功能的重要性。     

信号计算机联锁系统安全性可靠性分析

结合燕化铁路的现状,总结近年来燕化铁路计算机联锁系统可靠性下降的原因,并将双机热备系统的可靠性和安全性与二乘二取二、三取二系统做MATLAB仿真比较,提出改良现有计算机联锁系统的建议.     

CTC测试平台结构分析与设计

CTC系统主要负责将阶段计划自动转化为进路命令发送给车站联锁系统来实现对列车的调度,是CTCS-3级列控系统的重要组成部分.本文主要给出了CTC系统在测试环境下的平台设计方案,以及对此平台的具体搭建过程研究.服务器及自律机的设计采用稳定性好且安全性高的Linux系统.最后还提出了2种关于CTC系统整体校时的方法.结果表明该方案在保证安全的前提条件下使系统能够更为快捷高效的完成功能测试.     

基于窄带物联网的全电子联锁远程监测系统研究

伴随全电子联锁系统的推广应用,针对实时监测系统运行状态和及时有效进行设备维护的需求,结合全电子联锁系统执行单元特点并采用窄带物联网技术,从系统软硬件两方面研究设计了一种全电子联锁远程监测系统。在此基础上,通过对系统在交互通信时数据传输过程可能存在遭受窃取、伪造等安全风险的分析,提出系统通信数据的加密模型并优化了密钥更新算法。系统测试、通信数据加密模型及密钥更新算法验证结果表明,研究的全电子联锁远程监测系统能够实现实时监测全电子联锁系统设备并将设备状态或故障信息安全传输和显示于用户终端,提出的通信数据加密模型及密钥更新算法能够有效地保障通信数据的传输安全,系统设计能够满足铁路安全运营和维护的需要。