| 致谢 | 第7-8页 |
| 摘要 | 第8-9页 |
| abstract | 第9-10页 |
| 第一章 绪论 | 第17-22页 |
| 1.1 课题背景以及意义 | 第17-18页 |
| 1.1.1 研究背景 | 第17-18页 |
| 1.1.2 研究目的和意义 | 第18页 |
| 1.2 系统建模形式化方法的研究现状 | 第18-20页 |
| 1.3 论文主要工作 | 第20-21页 |
| 1.4 本文章节安排 | 第21-22页 |
| 第二章 Event-B形式化语言和Rodin平台 | 第22-34页 |
| 2.1 Event-B数学体系 | 第22-27页 |
| 2.1.1 谓词和布尔值 | 第22-23页 |
| 2.1.2 集合 | 第23-24页 |
| 2.1.3 关系 | 第24-26页 |
| 2.1.4 算术和赋值 | 第26-27页 |
| 2.2 Event-B形式化开发方法 | 第27-32页 |
| 2.2.1 简介 | 第27-29页 |
| 2.2.2 场景 | 第29-30页 |
| 2.2.3 机器 | 第30-31页 |
| 2.2.4 事件 | 第31-32页 |
| 2.3 Rodin平台及插件 | 第32-33页 |
| 2.3.1 Rodin平台 | 第32-33页 |
| 2.3.2 主要插件 | 第33页 |
| 2.4 本章小结 | 第33-34页 |
| 第三章 机车运输信号系统的Event-B建模 | 第34-49页 |
| 3.1 轨道机车运输信号平面布置图建模 | 第34-38页 |
| 3.1.1 初步建模 | 第34-35页 |
| 3.1.2 模型扩展 | 第35-36页 |
| 3.1.3 平面布置图具体模型 | 第36-38页 |
| 3.2 运输信号平面布置图Rodin模型自动生成 | 第38-41页 |
| 3.2.1 AutoCAD中的平面布置图转成Excel表格 | 第38-39页 |
| 3.2.2 Rodin平台中Java操作Excel表格 | 第39-41页 |
| 3.3 联锁表模型建立 | 第41-45页 |
| 3.3.1 联锁表术语简介 | 第41-43页 |
| 3.3.2 Rodin平台下联锁表模型 | 第43-45页 |
| 3.4 Excel形式的联锁表自动生成Rodin模型 | 第45-48页 |
| 3.4.1 联锁表内容获取 | 第46页 |
| 3.4.2 模型自动写入Rodin平台中 | 第46-48页 |
| 3.5 本章小结 | 第48-49页 |
| 第四章 煤矿井下机车车辆运输信号设计规范Event-B建模 | 第49-57页 |
| 4.1 煤矿井下机车车辆运输信号设计规范 | 第49-53页 |
| 4.1.1 区段、进路与联锁设计 | 第49-51页 |
| 4.1.2 信号机 | 第51-52页 |
| 4.1.3 道岔与转辙装置 | 第52页 |
| 4.1.4 车位传感器与无线收发信装置 | 第52-53页 |
| 4.2 设计规范建模 | 第53-56页 |
| 4.2.1 敌对进路模型 | 第53-54页 |
| 4.2.2 区段空闲检查模型 | 第54-55页 |
| 4.2.3 信号机模型 | 第55页 |
| 4.2.4 联锁道岔以及车位传感器模型 | 第55-56页 |
| 4.3 本章小结 | 第56-57页 |
| 第五章 联锁表验证与检错 | 第57-70页 |
| 5.1 模型证明原理 | 第57-63页 |
| 5.1.1 Rodin核心 | 第57-58页 |
| 5.1.2 Event-B库包和Event-B核心 | 第58-59页 |
| 5.1.3 图形用户界面 | 第59页 |
| 5.1.4 证明义务 | 第59-63页 |
| 5.2 联锁表正确性验证 | 第63-64页 |
| 5.2.1 ProB插件 | 第63页 |
| 5.2.2 具体联锁表验证结果 | 第63-64页 |
| 5.3 联锁表检错 | 第64-69页 |
| 5.3.1 语法或书写检错 | 第64-65页 |
| 5.3.2 THM证明义务检错 | 第65-69页 |
| 5.4 本章小结 | 第69-70页 |
| 第六章 总结与展望 | 第70-72页 |
| 6.1 课题总结 | 第70页 |
| 6.2 课题展望 | 第70-72页 |
| 参考文献 | 第72-75页 |
| 攻读硕士学位期间的学术活动及成果情况 | 第75-77页 |
