论文部分内容阅读
城市轨道交通因其运量大、占地少、高效节能、有利于保护环境等优点,当前已成为各大城市缓解交通拥堵压力的首选方案。基于通信的列车控制系统(Communication-based Train Control, CBTC)利用通信技术实现车-地之间双向大容量的信息交互,具有安全、高效、灵活的特点,在城市轨道交通中得到了广泛应用。计算机联锁(Computer-based Interlocking, CBI)系统是CBTC的关键系统,通过对道岔、区段、信号等轨旁设备进行监控完成列车运行预排、过程监控等功能。CBI系统是一种安全苛求性系统,须要不断的提高系统安全性来适应城市轨道交通的发展。传统的软件设计及测试方法已经无法满足CBI系统繁杂地联锁控制逻辑及以故障安全为中心的安全需求。基于模型的软件开发方法近年来在安全关键领域逐渐被接受。高安全性应用开发环境(Safety Critical Application Development Environment, SCADE),以基于模型的开发方式为安全苛求系统提供完整的嵌入式开发解决方法,其内置的仿真器以及形式化验证器在软件安全性和功能性上提供保证。本文基于SCADE对CBI系统联锁逻辑进行建模、仿真及形式化验证,以此保障其安全性。本次论文主要工作有：(1)介绍CBTC系统及其组成。(2)分析CBTC系统联锁逻辑、基于CBTC的联锁特点功能以及CBTC系统中联锁与其他子系统的信息交互。(3)以进路建立过程为例,解析进路建立过程中联锁的功能需求,将功能需求划分为道岔模块、进路模块和信号模块三部分进行详细介绍。(4)研究SCADE理论基础,重点研究基于数据流图的建模方法以及仿真和形式化验证过程。(5)利用SCADE数据流图建模方式对联锁进行模块化设计并据此建立模型。通过仿真保证所建模型无错误,通过形式化验证证明所建模型符合联锁安全需求。