高速铁路计算机联锁软件应用数据安全防护方法研究

为提高工程应用中联锁软件的可靠性和安全性,依据铁路信号系统故障-安全设计原则,研究应用数据的安全防护方法。基于站场图形网络结构的联锁数据特点,采用CRC、正发码校验等方法有效避免软件接口数据配置错误;利用标准程序模块生成的动态数据与静态数据的相互校验,有效验证联锁数据的逻辑正确性。这种安全防护方法在工程实践中得到广泛应用并验证,以较小的代价提高了联锁软件质量。此外,基于联锁系统二取二安全冗余原理,提出在软件编制过程中采用双人编制的冗余工作模式,大大降低了数据编制中人为错误发生的概率。     

车地协同下的联锁子系统HCPN建模与验证

联锁子系统作为站内行车安全的关键保障,是车地协同下的列车运行控制系统的重要组成部分。传统联锁子系统存在地面集中控制失效风险大、列车自主化程度低等不足,为顺应精简系统结构、降低运营成本和提升列车自主化的列控技术发展趋势,设计一种车地协同下的联锁子系统用于城际铁路。考虑多车间的进路冲突是影响子系统功能实现的关键因素,提出进路预延伸策略以避免列车间的进路冲突。为确保联锁子系统功能安全,采用一种基于层次着色Petri网(HCPN)的系统功能建模与验证方法。通过对联锁子系统的主要功能实现过程—进路建立过程进行分析,提取子系统的功能需求,以此建立顶层需求模型。为缩小底层实现与顶层需求之间的差距,建立基于数据及行为低抽象度表达的模块层模型,并在其中引入死锁控制策略实现对系统功能逻辑的完整表达。以冲突进路建立场景为模型的输入参数,执行验证过程,通过对模型标准状态空间性能分析,实现对模型正确性的检验。在此基础上,采用分支时序逻辑ASK-CTL公式与状态空间搜索算法相结合的验证方法,完成对子系统功能安全性的检验。研究结果表明:模型的行为特性同子系统预期相一致,能够正确表达系统的行为。所设计子系统满足功能安全需求,可为底层实现提供依据。     

联锁软件的Petri网形式化定义

用Petri网对联锁系统中的核心部分－联锁机中的联锁软件进行表式化定义和分析，以减少联锁系统中的不确定性因素，降低联锁软件的复杂性，保证联锁软件定义的正确性，并对该定义进行了形式化验证。同时以进程建立过程作为事例，说明了用Petri我形式化定义联锁软件的具体过程，采用分层模型化技术对联锁软件中的各个变迁（模块）进行逐级分解和验证，最终得到经过验证的，足够详细的联锁软件模型，利用该模型能对系统的一些重要性能（如安全性和实时性）进行分析和改进。     

基于沙盘的城轨控制实验室集中站联锁仿真系统

在城轨控制实验室仿真平台中,集中站联锁系统是保障列车各种作业安全的重要子系统.本文运用UML建模方法和Visio工具,对系统的需求、设计、编程实现和测试过程进行了描述和分析,建立了系统不同设计阶段的可视化模型.选取沙盘上2个典型集中站进行编程实现和测试,验证了运用UML方法对系统建模的正确性,且能够与沙盘联动控制.此外,系统还设计并实现了保护区段和侧面防护,这是地铁联锁系统的独有特点.     

站场形数据结构在车站信号实训系统中的实现

计算机联锁系统是负责处理进路内的道岔、信号机、轨道电路之间安全联锁关系的系统。本文通过对比计算机联锁中总进路表和站场形数据结构两种实现方法各自的特点,选择了站场形数据结构进行数据的存储和进路的搜索,并在高铁车站信号实训系统实现,验证了该方法的可行性和合理性。     

基于Event-B的计算机联锁安全规范描述与验证

本文结合具体的站场实例,基于Event-B方法对信号开放、道岔控制、进路解锁等联锁系统关键安全规范进行了形式化模型描述和验证分析,给出了严格的分析结果.工作表明,铁路信号联锁系统是具有复杂时序逻辑的控制系统,Event-B方法适合于该类系统的描述与验证.通过形式化的联锁安全规范描述与验证,可以在系统开发的早期及时发现设计错误或漏洞,有助于提高计算机联锁系统的软件开发质量.     

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

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

基于通信顺序进程与B方法的CBTC计算机联锁系统的形式化建模与验证

针对CBTC联锁系统的复杂性,提出一种基于通信顺序进程(CSP)与B方法集成的形式化方法,即在通信顺序进程的通信事件与B方法抽象机的操作之间建立起一对一的映射关系,实现通信事件通过控制抽象机的操作、进而影响抽象机状态的目标,从而实现通信顺序进程和B方法之间的同步。以1个实际站场为例,采用B方法对具有复杂状态空间的CBTC联锁系统的逻辑状态运算建立抽象机,采用通信顺序进程对CBTC联锁系统与外部系统的并发交互行为建立进程,并通过映射关系使CBTC联锁系统的抽象机与外部交互行为进程同步,由此建立基于通信顺序进程与B方法的CBTC联锁系统的形式化模型。采用ProB工具对建立的CBTC联锁系统模型的安全性、无死锁性进行验证。发现并修改模型中的不一致、不完全、歧义等错误,从而验证了CBTC联锁系统的安全性和无死锁性,保证了系统的最终实现。     

铁路站场信号联锁关系自动生成算法研究

当站场结构发生变化,站场联锁关系表也随之改变需重新编写,而站场联锁表多依靠深度搜索或广度搜索算法来生成,对于大型编组站其计算量大、效率较低。通过对铁路站场运输设备及其相互间关系的研究,分析站场拓扑结构,进行有向图建模,应用图论的最优化理论探讨铁路站场联锁表的自动生成方法。并且通过对图搜索算法的研究和对比,设计启发式的联锁表进路搜索方法,实现联锁表的准确、高效自动生成。     

计算机联锁数据自动生成软件的设计与实现

针对计算机联锁系统数据编写任务量大、正确性和安全性要求高等情况,通过分析联锁系统数据的结构特点,结合可视化编程方法,开发一种自动化软件,实现铁路车站图形绘制和联锁数据生成与校验功能.测试与应用表明,该软件可有效避免联锁数据编制中的人为错误,提高联锁软件安全可靠度,同时降低了联锁软件编制人员的专业水平门槛,可缩短软件编制...     

调车监控系统模拟平台联锁模拟模块的实现

联锁模拟模块是STP-yh型无线调车机车信号和监控系统模拟测试平台的基础模块,是运用联锁的基本逻辑原理和面向对象的软件编程方法,来实现站场中的联锁设备的模拟运作。     

基于二叉树结构的城轨沙盘联锁系统设计

二叉树在计算机联锁中有着较多的应用,根据二叉树的结构,将城市轨道交通线路信号点抽象成二叉树节点,构建线路的二叉树模型,然后在二叉树前序遍历的基础上设计正向搜索算法和逆向搜索算法,完成进路搜索功能,既能高效地实现联锁功能又能保障进路的安全性。文章选取城轨控制实验室沙盘2号线金顶集中站进行二叉树型数据结构建模,采用VB软件完成系统的人机界面和主要联锁功能模块的设计。     

基于自动Petri网的联锁逻辑设计

联锁软件的逻辑严密性和安全性对于行车有很大的影响。利用自动化Petri网,根据轨道电路、信号机和道岔之间相互制约的关系以及状态的转换,分别建立了信号机、道岔和进路模型,并根据列车的运行状态细化模型从列车压入进路到出清进路的过程,建立进路解锁的模型。基于上述分析,设计了一种基于可编程逻辑控制器的联锁软件设计方案,实现对联锁的逻辑控制。     

联锁系统逻辑测试方法研究

联锁系统是轨道交通列车运行控制系统的重要组成部分,它对列车的运行安全和效率有重要的影响.目前,地铁联锁测试通常归结于对系统进行相应的场景复现,按照测试序列对进路进行相应的操作,观察联锁的逻辑是否正确.根据该测试方法编制的测试序列,测试内容重复,测试效率较低.本文采用等价类划分方法的思想,对地铁联锁系统的测试需求进行归类,优化了测试序列,提高了测试效率,并且以北京地铁亦庄站的联锁系统测试进行了验证.     

关于城市轨道交通CBTC计算机联锁子系统的研究

近年来,基于通信的列车控制技术(CBTC)以其显著优势,逐渐成为城市轨道交通信号系统的首选方案。传统的联锁技术无法支撑CBTC信号系统的安全、高效、高自动化的要求。CBTC信号系统中的联锁子系统不仅要提供联锁逻辑保障,还要支持移动闭塞、点式ATP控制、以及不同模式列车的混跑等需求。文章简要介绍了基于CBTC技术的国产化联锁系统的架构、功能方面的创新和技术特点等。     

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

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

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

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

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

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

联锁表自动生成软件的设计与实现

为提高铁路信号设计效率,设计联锁表自动生成软件。依据计算机联锁车站联锁图表编制原则,运用绘图交换格式(DXF)数据提取的方法,结合车站信号设备平面布置图及其他站场数据,构建站场形数据结构,通过广度优先搜索算法,实现进路自动搜索并保存进路数据和联锁表数据,利用ActiveX技术与AutoCAD软件连接,根据保存的联锁表数据,生成并输出CAD格式的联锁表。联锁表自动生成软件已应用于现场,取得了良好的应用效果。