论文部分内容阅读
城市轨道交通以其安全可靠、污染低、运量大、速度快、受其他交通方式干扰小等特点,成为解决城市交通拥堵问题的首选方案。基于通信的列车控制系统(Communication-based Train Control, CBT C)具有轨旁设备少、列车追踪间隔短、运营效率高等优点,是列控技术的重要发展方向。计算机联锁(Computer Based Interlocking, CBI)系统作为CBTC的核心子系统之一,是一个安全苛求系统,对列车的安全运行有着重要的影响,具有极高的安全性和可靠性要求,因此,如何保证计算机联锁系统设计开发的安全性和正确性具有十分重要的意义。安全状态机(Safe State Machine, SSM)是一种图形化的同步建模语言,具有并发性、层次性、良好的优先级抢占机制和通信机制,模型清晰、简洁,具有良好的可读性,能够描述安全苛求系统复杂的逻辑过程。SSM形式化的理论基础避免了传统需求分析方法中的模糊性和二义性等缺陷；同时,高安全性应用开发环境(Safety Critical Application Development Environment, SCADE)支持SSM的建模、仿真和形式化验证,为SSM在实际工程中的应用提供了基础。本文选择SSM来对CBI系统进行建模和分析,主要包括以下几个方面：(1)分析了SSM的理论基础、建模特征及格局转移机制,并介绍了SSM在SCADE中的建模、仿真及形式化分析方法；(2)分析了CBI的基本结构及CBTC系统中的CBI的联锁功能,分析了CBI与CBTC子系统的交互关系,对比了CBTC下CBI与传统的联锁系统的区别。(3)将CBI划分为道岔、进路、信号机三个功能模块,分析了各个模块具体的逻辑条件；然后基于SSM的理论,利用SCADE对各个模块进行了建模,具体包括道岔请求、选排、锁闭逻辑,进路请求、检查逻辑,区段方向逻辑及信号开放逻辑等；最后利用SCADE的数据流图将道岔、进路及信号机三个模块集成为CBI逻辑模型。(4)通过SCADE提供的仿真器对模型进行仿真,检查CBI模型的正确性；然后提取系统的安全属性,利用SCADE的形式化验证器对模型进行形式化验证,证明模型满足预期安全需求,保证了模型的安全性和正确性。