| 摘要 | 第6-7页 |
| Abstract | 第7页 |
| 第1章 绪论 | 第10-14页 |
| 1.1 研究背景及意义 | 第10-11页 |
| 1.2 国内外研究现状 | 第11-12页 |
| 1.2.1 联锁国内外发展现状 | 第11页 |
| 1.2.2 形式化方法在计算机联锁系统中的研究现状 | 第11-12页 |
| 1.3 论文主要内容及结构 | 第12-14页 |
| 第2章 高安全性应用开发环境 | 第14-25页 |
| 2.1 SCADE概述 | 第14页 |
| 2.2 SCADE软件开发模式 | 第14-16页 |
| 2.2.1 传统“V”型软件开发模式 | 第14-15页 |
| 2.2.2 SCADE“Y”型软件开发模式 | 第15-16页 |
| 2.3 SCADE Suite功能详解 | 第16-19页 |
| 2.3.1 需求管理 | 第16-17页 |
| 2.3.2 模型仿真 | 第17页 |
| 2.3.3 形式化验证 | 第17-18页 |
| 2.3.4 代码生成模块 | 第18-19页 |
| 2.4 SCADE建模机制 | 第19-25页 |
| 2.4.1 同步假设 | 第19-20页 |
| 2.4.2 数据流图 | 第20-22页 |
| 2.4.3 安全状态机 | 第22-25页 |
| 第3章 计算机联锁系统逻辑 | 第25-34页 |
| 3.1 计算机联锁系统概述 | 第25-26页 |
| 3.2 计算机联锁系统的特点 | 第26页 |
| 3.3 计算机联锁系统软件功能 | 第26-34页 |
| 3.3.1 进路建立子系统 | 第27-31页 |
| 3.3.2 进路解锁子系统 | 第31-34页 |
| 第4章 基于SCADE的计算机联锁系统建模 | 第34-56页 |
| 4.1 计算机联锁系统需求管理 | 第34-36页 |
| 4.2 计算机联锁系统建模 | 第36-56页 |
| 4.2.1 计算机联锁系统集层模型 | 第36-42页 |
| 4.2.2 进路选择模块 | 第42-47页 |
| 4.2.3 进路锁闭模块 | 第47-48页 |
| 4.2.4 信号开放模块 | 第48-50页 |
| 4.2.5 信号开放保持模块 | 第50-52页 |
| 4.2.6 正常通过解锁模块 | 第52-54页 |
| 4.2.7 取消进路模块 | 第54-56页 |
| 第5章 基于SCADE的计算机联锁模型验证 | 第56-67页 |
| 5.1 计算机联锁系统模型覆盖率分析 | 第56-58页 |
| 5.2 计算机联锁系统仿真分析 | 第58-61页 |
| 5.3 计算机联锁系统形式化验证 | 第61-64页 |
| 5.4 计算机联锁软件代码生成 | 第64-67页 |
| 结论 | 第67-68页 |
| 致谢 | 第68-69页 |
| 参考文献 | 第69-72页 |
| 附录1 计算机联锁形式化验证结果 | 第72-73页 |
| 附录2 计算机联锁集成模型仿真场景 | 第73-76页 |