基于安全状态机的计算机联锁系统建模与分析

摘要

城市轨道交通以其安全可靠、污染低、运量大、速度快、受其他交通方式干扰小等特点，成为解决城市交通拥堵问题的首选方案。基于通信的列车控制系统(Communication-based Train Control，CBTC)具有轨旁设备少、列车追踪间隔短、运营效率高等优点，是列控技术的重要发展方向。计算机联锁(ComputerBased 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的形式化验证器对模型进行形式化验证，证明模型满足预期安全需求，保证了模型的安全性和正确性。

目录

声明

摘要

第1章 绪论

1．1 研究背景及意义

1．2 国内外研究现状

1．2．1 计算机联锁系统发展现状

1．2．2 形式化方法在铁路信号系统中的研究现状

1．3 论文主要内容与结构

第2章 安全状态机与SCADE

2．1 形式化方法概述

2．2 安全状态机理论

2．2．1 同步假设

2．2．2 安全状态机概述

2．2．3 安全状态机特征

2．2．4 格局转移机制

2．3 SCADE

2．3．1 SCADE概述

2．3．2 安全状态机仿真

2．3．3 SCADE形式化验证

第3章 计算机联锁系统分析

3．1 计算机联锁系统概述

3．1．1 计算机联锁系统结构

3．1．2 计算机联锁系统的冗余设计

3．2 CBTC系统概述

3．2．1 CBTC系统结构

3．2．2 CBTC系统的联锁功能

3．2．3 计算机联锁与CBTC子系统的信息交互

3．3 CBTC计算机联锁系统与传统联锁系统的区别

3．3．1 结构区别

3．3．2 功能区别

第4章 基于安全状态机的计算机联锁系统建模

4．1 计算机联锁模块划分

4．2 道岔模块

4．2．1 道岔需求

4．2．2 道岔请求命令执行

4．2．3 道岔选排一致

4．3 进路模块

4．3．1 进路请求

4．3．2 道岔锁闭

4．3．3 进路检查

4．3．4 接近联锁

4．3．5 区段方向联锁

4．3．6 站台安全状态

4．4 信号机模块

4．5 集成模块

第五章 计算机联锁系统模型验证与分析

5．1 计算机联锁系统模型仿真

5．1．1 道岔模块仿真

5．1．2 计算机联锁集成模型仿真

5．2 计算机联锁系统模型形式化验证

5．2．1 SCADE形式化验证与仿真

5．2．2 SCADE形式化验证流程

5．2．3 计算机联锁形式化验证

结论

致谢

参考文献

附录

攻读硕士学位期间发表的论文