基于Event-B的联锁系统进路控制建模与验证研究
| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-11页 |
| 1 绪论 | 第11-18页 |
| ·选题的背景和意义 | 第11-15页 |
| ·联锁系统发展概述 | 第11-12页 |
| ·计算机联锁系统软件设计开发存在的问题 | 第12-14页 |
| ·形式化方法的引入 | 第14-15页 |
| ·国内外研究现状 | 第15-16页 |
| ·论文的研究内容和组织结构 | 第16-18页 |
| 2 Event-B方法相关理论及工具 | 第18-32页 |
| ·Event-B形式化建模方法 | 第18-26页 |
| ·数学概念和符号体系 | 第18-21页 |
| ·Event-B模型基本元素和结构 | 第21-24页 |
| ·Event-B模型的精化 | 第24-26页 |
| ·Event-B形式化验证方法 | 第26-28页 |
| ·Event-B的证明义务机制 | 第26-27页 |
| ·证明过程 | 第27-28页 |
| ·Rodin平台及相关工具 | 第28-31页 |
| ·Rodin 平台 | 第28-30页 |
| ·UML-B工具介绍 | 第30-31页 |
| ·本章小结 | 第31-32页 |
| 3 基于Event-B的联锁进路控制过程建模 | 第32-61页 |
| ·基于Event-B的联锁软件形式化开发方法 | 第32页 |
| ·联锁进路控制过程分析 | 第32-39页 |
| ·进路建立阶段 | 第33-37页 |
| ·进路解锁阶段 | 第37-39页 |
| ·模型精化策略的制定 | 第39-40页 |
| ·联锁进路控制Event-B模型的建立 | 第40-60页 |
| ·联锁进路控制中的建模元素分析 | 第40-42页 |
| ·进路控制模型的基本场景 | 第42-45页 |
| ·进路选排的Event-B模型 | 第45-49页 |
| ·进路锁闭的Event-B模型 | 第49-53页 |
| ·信号控制的Event-B模型 | 第53-55页 |
| ·进路自动解锁的Event-B模型 | 第55-57页 |
| ·取消进路和人工延时解锁的Event-B模型 | 第57-60页 |
| ·本章小结 | 第60-61页 |
| 4 联锁进路控制模型的形式化验证 | 第61-76页 |
| ·联锁进路控制模型的仿真 | 第61-69页 |
| ·UML-B状态机仿真的概念和方法 | 第61-63页 |
| ·进路控制Event-B模型的仿真 | 第63-69页 |
| ·联锁进路控制模型证明义务的证明 | 第69-74页 |
| ·模型证明义务的生成 | 第69-70页 |
| ·证明义务的自动证明 | 第70-71页 |
| ·证明义务的交互式证明 | 第71-74页 |
| ·本章小结 | 第74-76页 |
| 5 总结与展望 | 第76-79页 |
| ·论文总结 | 第76页 |
| ·展望 | 第76-79页 |
| 参考文献 | 第79-81页 |
| 图索引 | 第81-83页 |
| 表索引 | 第83-85页 |
| 作者简历 | 第85-89页 |
| 学位论文数据集 | 第89页 |
