| 摘要 | 第6-7页 |
| Abstract | 第7页 |
| 第1章 绪论 | 第10-13页 |
| 1.1 研究背景及意义 | 第10-11页 |
| 1.2 国内外研究现状 | 第11-12页 |
| 1.2.1 计算机联锁系统发展现状 | 第11页 |
| 1.2.2 形式化方法在铁路信号系统中的研究现状 | 第11-12页 |
| 1.3 论文主要内容与结构 | 第12-13页 |
| 第2章 安全状态机与SCADE | 第13-24页 |
| 2.1 形式化方法概述 | 第13页 |
| 2.2 安全状态机理论 | 第13-22页 |
| 2.2.1 同步假设 | 第13-14页 |
| 2.2.2 安全状态机概述 | 第14-17页 |
| 2.2.3 安全状态机特征 | 第17-19页 |
| 2.2.4 格局转移机制 | 第19-22页 |
| 2.3 SCADE | 第22-24页 |
| 2.3.1 SCADE概述 | 第22-23页 |
| 2.3.2 安全状态机仿真 | 第23页 |
| 2.3.3 SCADE形式化验证 | 第23-24页 |
| 第3章 计算机联锁系统分析 | 第24-33页 |
| 3.1 计算机联锁系统概述 | 第24-27页 |
| 3.1.1 计算机联锁系统结构 | 第24-25页 |
| 3.1.2 计算机联锁系统的冗余设计 | 第25-27页 |
| 3.2 CBTC系统概述 | 第27-31页 |
| 3.2.1 CBTC系统结构 | 第27-28页 |
| 3.2.2 CBTC系统的联锁功能 | 第28-30页 |
| 3.2.3 计算机联锁与CBTC子系统的信息交互 | 第30-31页 |
| 3.3 CBTC计算机联锁系统与传统联锁系统的区别 | 第31-33页 |
| 3.3.1 结构区别 | 第31页 |
| 3.3.2 功能区别 | 第31-33页 |
| 第4章 基于安全状态机的计算机联锁系统建模 | 第33-56页 |
| 4.1 计算机联锁模块划分 | 第33-34页 |
| 4.2 道岔模块 | 第34-39页 |
| 4.2.1 道岔需求 | 第34-36页 |
| 4.2.2 道岔请求命令执行 | 第36-37页 |
| 4.2.3 道岔选排一致 | 第37-39页 |
| 4.3 进路模块 | 第39-52页 |
| 4.3.1 进路请求 | 第39-40页 |
| 4.3.2 道岔锁闭 | 第40-41页 |
| 4.3.3 进路检查 | 第41-43页 |
| 4.3.4 接近联锁 | 第43-46页 |
| 4.3.5 区段方向联锁 | 第46-51页 |
| 4.3.6 站台安全状态 | 第51-52页 |
| 4.4 信号机模块 | 第52-54页 |
| 4.5 集成模块 | 第54-56页 |
| 第5章 计算机联锁系统模型验证与分析 | 第56-65页 |
| 5.1 计算机联锁系统模型仿真 | 第56-59页 |
| 5.1.1 道岔模块仿真 | 第56-58页 |
| 5.1.2 计算机联锁集成模型仿真 | 第58-59页 |
| 5.2 计算机联锁系统模型形式化验证 | 第59-65页 |
| 5.2.1 SCADE形式化验证与仿真 | 第59-60页 |
| 5.2.2 SCADE形式化验证流程 | 第60-61页 |
| 5.2.3 计算机联锁形式化验证 | 第61-65页 |
| 结论 | 第65-66页 |
| 致谢 | 第66-67页 |
| 参考文献 | 第67-70页 |
| 附录1 道岔模型测试用例 | 第70-73页 |
| 附录2 集成模型测试用例 | 第73-81页 |
| 附录3 道岔模块安全属性及形式化验证结果 | 第81-82页 |
| 附录4 进路模块安全属性及形式化验证结果 | 第82-84页 |
| 附录5 信号机模块安全属性及形式化验证结果 | 第84-85页 |
| 附录6 集成模块安全属性及形式化验证结果 | 第85-86页 |
| 攻读硕士学位期间发表的论文 | 第86页 |