共查询到18条相似文献,搜索用时 140 毫秒
1.
计算机联锁系统是铁路信号控制系统的核心设备,是有着苛刻安全要求的复杂控制系统。本文采用Prover形式化开发工具对联锁软件安全需求进行形式化验证。通过模型检验的形式化验证方法,遍历系统输入变量的所有状态空间.验证联锁特定应用满足系统安全需求,确保系统的安全性得以正确实现。在保证系统安全性的基础上,以全状态空间查找反例的检验方法进一步提升产品的质量。 相似文献
2.
3.
4.
5.
针对目前计算机联锁系统建模与验证难度较大的问题,提出一种UML(Unified Modeling Language)与NuSMV(New Symbolic Model Verifier)相结合的计算机联锁模型形式化检验方法。以一个标准站场中的一条接车进路建立过程为例,对联锁系统需求进行分析并通过UML建立相应的模型,再列出它与NuSMV之间的映射关系并实现将UML模型自动转换为NuSMV形式化模型,最后完成对计算机联锁系统的验证,检测其需求中可能存在的漏洞。该方法能够降低对计算机联锁系统形式化建模与验证的难度与减少人工建模时可能出现的错误,为计算机联锁系统形式化模型的建立与验证提供一种新思路。 相似文献
6.
CBTC的计算机联锁(CBI)系统是一个复杂且安全性要求非常高的系统,若按照传统的方法进行开发,很难达到其所需要的安全性和可靠性.本文提出基于高安全性应用程序开发环境(SCADE)开发城轨联锁系统软件的方法,能有效解决上述问题.文章主要介绍基于SCADE开发CBI软件的流程,建模方法,形式化验证和代码自动生成的方法. 相似文献
7.
针对CBTC联锁系统的复杂性,提出一种基于通信顺序进程(CSP)与B方法集成的形式化方法,即在通信顺序进程的通信事件与B方法抽象机的操作之间建立起一对一的映射关系,实现通信事件通过控制抽象机的操作、进而影响抽象机状态的目标,从而实现通信顺序进程和B方法之间的同步。以1个实际站场为例,采用B方法对具有复杂状态空间的CBTC联锁系统的逻辑状态运算建立抽象机,采用通信顺序进程对CBTC联锁系统与外部系统的并发交互行为建立进程,并通过映射关系使CBTC联锁系统的抽象机与外部交互行为进程同步,由此建立基于通信顺序进程与B方法的CBTC联锁系统的形式化模型。采用ProB工具对建立的CBTC联锁系统模型的安全性、无死锁性进行验证。发现并修改模型中的不一致、不完全、歧义等错误,从而验证了CBTC联锁系统的安全性和无死锁性,保证了系统的最终实现。 相似文献
8.
嵌入式联锁软件模拟自动测试平台的研究 总被引:2,自引:0,他引:2
为满足联锁软件黑箱测试的要求,对联锁软件安全性需求进行了分级形式化表达,阐述了嵌入式联锁软件模拟自动测试平台的分布式结构模型及其实现方案,最后,给出了自动测试平台得到的联锁软件分类测试结果。 相似文献
9.
10.
计算机联锁软件的Z规格说明 总被引:4,自引:0,他引:4
计算机联锁软件是一种典型的安全关键软件,具有非常复杂的联锁控制逻辑和以失效安全为核心的安全需求。形式化其安全需求是一件十分必要,也是一件十分艰巨的任务。本文使用形式化规格说明语言———Z语言来描述其安全需求,生成形式化规格说明。形式化规格说明不仅有助于提高计算机联锁软件的质量,而且也有利于将来对它进行更严格的测试。 相似文献
11.
张杰 《铁道标准设计通讯》2019,(11):165-171
铁路计算机联锁软件制作的关键数据,由手工输入,智能化水平不高。提出专家系统的思想,借助专家系统工具CLIPS,实现联锁站场特征的自动识别,数据的自动生成。将蓝图信息规范化,统一为Excel文件,解决了联锁知识的概念化及形式化问题。采用面向对象的知识表示方法,借鉴ID3的分类算法,建立知识库。分类算法提高了规则的合法化及程序执行的效率。在站场特征识别问题上,先讨论了基于二叉树的实现方法,又叙述了直接利用CLIPS消息函数的方法,比较可得,消息函数的方法简洁,具有优越性。总结3类VC++和CLIPS交互技术,说明CLIPS嵌入到VC++是可行的。经检验,该专家系统可以初步解决计算机联锁数据标准化、自动化的问题。 相似文献
12.
13.
基于站场图形网络的计算机联锁软件在高速铁路的应用研究 总被引:3,自引:3,他引:0
《铁道标准设计通讯》2016,(9):141-145
为适应高速铁路列控系统接口需求,计算机联锁系统接入信号安全数据网[1]的同时,应用软件需要新增进路模块来实现接口的应用信息交互。进路模块利用原有联锁软件网络化结构的选路原理,实现了进路信息存储;利用进路中道岔的大号码特征,实现符合黄闪黄条件信号显示自动计算。软件采用模块化设计的同时,对软件需求、设计、结构、安全性进行全面分析,确保联锁子系统软件的兼容性和可持续开发性。基于升级的计算机联锁软件不仅满足高速铁路列车控制系统的需求,也提高了原有软件的安全性和可靠性。 相似文献
14.
结合计算机联锁系统的硬件和联锁软件的特征,介绍了软件的测试目的、步骤、黑盒测试中等价类划分法以及安全测试常用的故障树分析法。基于由测试软件、联锁软件和车站信号设备仿真系统组成的测试平台的联锁软件测试,在联锁软件黑盒测试覆盖率准则的基础上,举例介绍了用等价类划分法编写测试用例和用故障树分析法编写安全性测试用例以及测试流程,并用python伪代码实现了“进路正常选出”的测试用例。通过上面的方法来体现黑盒测试在计算机联锁软件逻辑运算功能的重要性。 相似文献
15.
城市轨道交通信号系统联锁控制权交接研究 总被引:2,自引:1,他引:1
《铁道标准设计通讯》2017,(9):138-143
城市轨道交通信号系统中,调度人员通过列车自动监控系统中心工作站和车站工作站都可以向联锁机发送控制命令,但是同一时刻联锁机只能有一个指令源。因此在设计联锁系统软件结构时,需要采用合理的联锁控制权交接机制,防止控制权交接错误。从联锁控制权交接问题入手,总结联锁控制权交接原则,详细分析各个设备之间采用不同互联方式时的联锁控制权交接方案,并对不同方案的影响和优缺点进行比较,为联锁系统的软件设计提供理论依据。 相似文献
16.
阐述了现有计算机联锁仿真软件的不足。重点介绍计算机联锁模块化仿真软件的开发。软件采用二级缓冲技术,具备真实室外环境和仿真环境的自适应能力。论述了该仿真系统实现的主要功能及特色。说明了该仿真系统在铁路信号中的应用前景。 相似文献
17.
城轨交通信号系统国产化是未来城市轨道建设的必然要求。讨论了作为信号系统核心子系统之一的计算机联锁设备与门设备的接口逻辑和联锁软件实现方法;阐述了计算机联锁应用层软件相关部分的设计方案,以适应城轨正线联锁设备的国产化要求。 相似文献
18.
基于VxWorks的计算机联锁控制系统软件研究 总被引:1,自引:1,他引:0
铁路车站信号计算机联锁控制系统是实时、多任务、安全苛求的计算机控制系统.分析DOS和Windows环境联锁控制软件设计存在的问题,结合VxWorks操作系统的特点,研究基于VxWorks实现联锁控制的可行性,在此基础上提出了一种VxWorks环境下设计联锁软件的方法,并进行了详细的系统设计.针对一个实际站场的编码测试结果表明,在VxWorks环境下更易于满足联锁软件对实时性、多任务调度的设计要求,并有利于提高系统的安全性. 相似文献