排序方式： 共有46条查询结果，搜索用时 218 毫秒
31.
联锁子系统作为站内行车安全的关键保障,是车地协同下的列车运行控制系统的重要组成部分。传统联锁子系统存在地面集中控制失效风险大、列车自主化程度低等不足,为顺应精简系统结构、降低运营成本和提升列车自主化的列控技术发展趋势,设计一种车地协同下的联锁子系统用于城际铁路。考虑多车间的进路冲突是影响子系统功能实现的关键因素,提出进路预延伸策略以避免列车间的进路冲突。为确保联锁子系统功能安全,采用一种基于层次着色Petri网(HCPN)的系统功能建模与验证方法。通过对联锁子系统的主要功能实现过程—进路建立过程进行分析,提取子系统的功能需求,以此建立顶层需求模型。为缩小底层实现与顶层需求之间的差距,建立基于数据及行为低抽象度表达的模块层模型,并在其中引入死锁控制策略实现对系统功能逻辑的完整表达。以冲突进路建立场景为模型的输入参数,执行验证过程,通过对模型标准状态空间性能分析,实现对模型正确性的检验。在此基础上,采用分支时序逻辑ASK-CTL公式与状态空间搜索算法相结合的验证方法,完成对子系统功能安全性的检验。研究结果表明：模型的行为特性同子系统预期相一致,能够正确表达系统的行为。所设计子系统满足功能安... 相似文献
32.
介绍了FSA方法的基本概念及在船舶安全领域中的应用,对应用中存在的问题进行了分析,并提出相应对策。 相似文献
33.
黑白数字图像的有穷状态自动机表示方法 总被引：2，自引：0，他引：2
自动机理论是理论计算机科学的基础理论之一，在很多领域自动机有着广泛的应用，在将黑白图像进行像素地址编码的基础上使用语言来描述数字图像，从而得到用自动机来描述数字图像的方法，任意有穷分辨率黑白图像均可以用有穷状态自动机来表示，多分辨率图像能够用有穷状态自动机来描述当且仅当该图像中不同形状的子图像的个数为有限个． 相似文献
34.
正在建设的时速300 km/h以上的高速铁路已采用CTCS-3级列车运行控制系统.车地信息交互流程是影响CTCS-3级列控系统的效率、可靠性和安全性的主要因素之一.基于时间自动机理论对车地交互流程进行建模与验证具有重要意义.首先将车地交互流程分为4个典型的子流程：任务启动流程、正常行车流程、RBC切换流程和任务结束流程,然后针对这些子流程建立无线闭塞中心（RBC）、车载设备（ATP）和铁路专用移动通信网（GSM-R）的时间自动机网络模型,最后利用时间自动机模型验证工具UPPAAL进行仿真分析,验证了CTCS-3级列控系统的车地交互流程的安全性和受限活性. 相似文献
35.
CBTC的计算机联锁(CBI)系统是一个复杂且安全性要求非常高的系统,若按照传统的方法进行开发,很难达到其所需要的安全性和可靠性.本文提出基于高安全性应用程序开发环境(SCADE)开发城轨联锁系统软件的方法,能有效解决上述问题.文章主要介绍基于SCADE开发CBI软件的流程,建模方法,形式化验证和代码自动生成的方法. 相似文献
36.
形式化方法在列车运行控制系统中的应用 总被引：2，自引：0，他引：2
为了确保列车运行控制系统设计和开发的正确性,比较了仿真、测试和形式化3种能够验证系统设计正确性的方式。根据列车运行控制系统对安全的苛求性,提出了4个与系统安全相关的重要特性,即实时性、混成性、分布(并发)性、反应性,并分析了与这些特性相关的具体形式化方法。通过对每种形式化方法的数学基础和应用范围的分析和归类,给出了各种方法的优势和不足。分析结果表明:任何形式化方法的应用都具有一定的局限性,这是由模型检验和定理证明的本质所决定的;指出了新方法提出、既有方法拓展以及多方法集成将是列车运行控制系统的形式化领域的方向。 相似文献
37.
本文通过介绍翻译发展的现状,论述了翻译中译外在中国发展的必然性,提出中译外发展的相关条件和面临的问题以及解决措施。 相似文献
38.
KZ4A型交流传动电力机车信息显示屏 总被引：2，自引：2，他引：0
介绍KZ4A型交流传动电力机车信息显示屏的硬件配置、工作原理,阐述根据哈萨克斯坦环境气候恶劣的特殊要求而作的主要材料的选型,论述双语言转换的软件实现功能,试验验证显示屏达到了低温指标。。 相似文献
39.
通过对社区卫生服务的功能需求出发,采用Z语言对系统规格进行了形式化说明,包括基础数据、系统状态以及系统操作等。采用形式化方法对社区卫生服务系统进行设计,能够得到一致的、精确的、简明的和无歧义的规格说明。 相似文献
40.
该文通过对目前立交运行中存在的不安全因素的分析,强调了立交设计应“以人为本”,树立安全至上的设计理念,注重安全性设计,并结合郑州中州大道与郑新快速通道立交工程来探讨立交设计中应遵循形式的统一性、路线的连续性、车道的平衡等基本原则. 相似文献