【摘 要】
：
区域控制器(ZC)是基于通信的列车自动控制(CBTC)信号系统中实现轨旁自动列车保护(ATP)功能的核心设备,用来计算列车移动授权以确保列车不发生冲撞,因此区域控制器软件实现的
【机 构】
：
卡斯柯信号技术有限公司北京市地铁运营有限公司地铁运营技术研发中心
【出 处】
：
2016年全国智慧城市与轨道交通学术会议
论文部分内容阅读
区域控制器(ZC)是基于通信的列车自动控制(CBTC)信号系统中实现轨旁自动列车保护(ATP)功能的核心设备,用来计算列车移动授权以确保列车不发生冲撞,因此区域控制器软件实现的正确性对于确保整个CBTC信号系统的安全起着极其重要作用.采用形式化证明技术可以弥补传统开发过程中验证手段(如测试)片面性的缺点,是对软件(系统)全状态空间的正确性验证,确保软件(系统)实现与需求一致性.文章介绍了一种基于模型开发软件的形式化证明方法,描述了形式化证明工具、证明义务结构及形式化证明流程,并以iZC200型区域控制器应用软件为例,说明如何精确描述待证明安全属性,不同类型模型形式化证明及其优化方法.
其他文献
本文以广州地铁7号线3标谢钟区间富水断裂破碎带施工为背景，浅析在此类地层中盾构施工的技术难点和技术措施，并对其施工方法、参数进行总结、分析，提出盾构机在富水断裂破碎带地
天津轨道交通网络化运营初步形成后,轨道交通路网客流出现急剧性增长特征.本文详细介绍天津轨道交通路网客流成长过程、发展规律和客流特征,同时对目前实际运营中存在的问题
针对以电压跌落、骤升、瞬时中断为代表的电梯暂态电能质量问题对城市轨道交通运营安全造成的影响,提出一种基于超级电容储能单元,并结合超宽范围Boost升压技术的快速检测方
本文分析了北京地铁5号线列车制动系统的概况及主要技术参数,介绍了国产化制动系统的组成、主要功能、试验验证等情况,认为该系统能够满足北京地铁5号线列车的制动性能要求。
使用三维建模软件CATIA对两种不同型号的城市轨道车辆转向架构架进行建模,基于工程模拟有限元软件ABAQUS对模型进行有限元分析;采用铁道车辆用转向架构架设计通则JISE4207标
随着我国铁路的不断提速,现行铁路道岔基本不能满足列车侧向高速通过的要求,提高道岔侧向高速通过能力是我国现在高速铁路发展必须解决的问题.现行铁路道岔虽然比以前有了很
为进一步提升安全管理工作水平,加强城市轨道交通运营企业运营安全风险管理,防范城市轨道交通事故发生,确保企业安全运营,安全风险预控管理成为城市轨道交通运营行业安全管理
本文简要介绍了综合监控系统及其集成的子系统BAS、FAS等,主要研究地铁综合监控系统的防雷技术,地铁综合监控防雷技术包括电源防雷和信号防雷,本文重点分析了信号防雷技术,并
津滨轻轨9号线车辆在外接电源箱检修作业中,发现1个外接电源箱箱盖正常锁闭时,在任意1个动车为主控端并操作升弓扳键,1、4车受电弓则会上升,给检修作业带来严重的安全隐患,直
微模块数据中心因其具备快速部署、高效节能、智能管理等优点,已成为当前及未来新一代数据中心建设的焦点和方向.本文通过对多个微模块数据中心建设的实际案例进行探讨,分析