【摘 要】
:
自主化CTCS-3级列控系统在确保高铁列车的安全运行方面起着至关重要的作用,有完全的自主产权,在软硬件设计以及功能需求上都新增了许多内容。因此,如何确保列控系统在新增规范要求下的安全性和可靠性就成为了重要的研究课题。同时对采用何种方法对列控系统安全因素进行分析在传统研究中并没有涉及,而形式化方法恰好弥补了这一不足,通过选取合适的形式化方法对列控系统进行建模及安全分析已成为目前列控系统安全保障技术的
论文部分内容阅读
自主化CTCS-3级列控系统在确保高铁列车的安全运行方面起着至关重要的作用,有完全的自主产权,在软硬件设计以及功能需求上都新增了许多内容。因此,如何确保列控系统在新增规范要求下的安全性和可靠性就成为了重要的研究课题。同时对采用何种方法对列控系统安全因素进行分析在传统研究中并没有涉及,而形式化方法恰好弥补了这一不足,通过选取合适的形式化方法对列控系统进行建模及安全分析已成为目前列控系统安全保障技术的主流研究趋势。本论文以自主化CTCS-3级列控系统轨道电路行车许可校验场景为研究对象,采用两种形式化方法对场景开展研究。首先提出基于时间自动机的建模方法,针对列控系统的实时性,分析场景下列控系统各设备的工作流程,经过合理的抽象简化后,利用时间自动机理论构建了轨道电路行车许可校验场景的时间自动机模型,在UPPAAL模拟器中对各模块交互情况进行仿真,使用验证器验证其安全功能属性和受限活性,证明了此建模方式的有效性,最后结合京沈客专辽宁段试验数据,编制轨道电路行车许可校验场景相关的测试序列,通过自主化CTCS-3级列控系统场景控制器开展仿真测试验证。同时利用UML(Unified Modeling Language,统一建模语言)扩展机制进行轨道电路行车许可校验场景安全分析。针对列控系统的混成性,对轨道电路行车许可校验场景进行分析,根据UML扩展机制对于建模的要求,前期包含UML场景类图以及状态转移图模型构建,对于系统中的状态迁移部分和动态连续过程结合故障扩展模型进一步描述其行为,在列控系统规范要求的基础上建立混成性概要描述文件,后期将已经建立好的模型利用混成自动机模型检验工具进行转换,分析轨道电路行车许可校验场景中可能出现的故障并进行描述,采用故障模型融合算法将PHAVer模型和故障模型融合来描述轨道电路行车许可校验场景中的故障情形和因为故障造成的场景功能影响,利用故障检测器对系统模型开始进行可达集计算,确定涉及系统安全的故障因素组合实现轨道电路行车许可校验场景的安全分析。结果表明,本文提出的方法可以满足轨道电路行车许可校验场景在列控系统需求设计阶段的安全特性要求,为以后列控系统的形式化建模与安全评估提供了参考方法。
其他文献
铁路路网的不断完善为出行提供便利服务的同时,高密度、大运量的铁路运输也为铁路工务工作提出了严峻的挑战。需要在各类自然环境下,较短天窗时间内完成铁路线路的检测工作。为克服传统接触式铁路线路检测效率低、安全性差、测量数据离散等缺陷,本文采用移动扫描测量系统快速、实时、高效的获取铁路点云数据,并针对海量点云数据设计快速、准确、系统的处理方法,实现铁路线路的一体化、智能化检测。为此,论文围绕移动扫描测量技
保障列车行车安全是铁路运营的前提,列车与运行前方物体冲撞是铁路安全事故的主要类型,为保证安全运行须对列车前方运行环境进行检测。现有且在用的铁路环境检测方式主要为人工巡线、易发生事故点安装视频监控或在山体桥隧等处架设防护网,显然,现有的防护手段已不能满足需求。本文提出图像和雷达数据融合的方式,随列车运行实时检测前方运行环境,及时有效检出前方障碍物,减轻或避免碰撞事故的后果。多传感器融合检测可弥补人眼
在高速铁路蓬勃发展的今天,作为其主要构成之一——信号系统愈发受到关注。道岔系统的正常、稳定、高效的工作则是保证信号系统安全的重要前提。自我国铁路行业建设运营以来,无论是纯粹的人工检修或者是现如今的微机监测结合个人经验完成检修,对于道岔系统的维检修工作主力依旧是现场工作人员通过人工观察、综合个人经验来完成。该方法容易受到工作人员现场经验、知识水平等因素的影响,导致结果出现滞后、错判、漏判等情况,并且
随着国内智慧停车场的建设以及高速公路电子不停车收费系统(electronic toll collection)的不断普及,对现有车牌识别技术的精度和速度方面提出了更高的要求,尤其在一些车牌字符模糊、检测环境复杂、光线不足等条件下。在识别精度方面,现有的大量商业车牌识别系统,其识别算法通常由两个处理步骤组成,即车牌定位和字符识别,两个步骤均对最终的识别结果起着极其关键的作用,因此增加识别系统的识别性
坝体溃决对水库下游居民的生命安全造成威胁,因此需要预先为下游居民规划合理的安全区,然后在受灾区和安全区之间规划高效的逃生路线。该问题涉及多个约束条件和优化目标,根据问题的发展现状,文章重点研究平坦区域多约束路径优化模型以及山地数字高程路径优化模型。首先,针对平坦区域多约束逃生路径优化问题建立了0-1整数规划模型,模型的目标函数是最小期望通行时间,为保证最终只生成最优路径引入了唯一通路选择约束,为避
随着科技的迅速发展和社会的不断进步,物流企业获得的利润不断提高,物流的合理化以及高效化也备受人们重视。合理的制定物流配送方案,有效降低配送成本,具有至关重要的理论价值和现实意义。传统的车辆路径问题(Vehicle Routing Problem,VRP)中货物的配送和回收是单独进行的,车辆在这种单独的作业模式下很容易出现空载、重复运输等造成浪费资源的情况,为了避免出现这种情况,许多企业考虑同时对货