| 致谢 | 第7-8页 |
| 摘要 | 第8-9页 |
| abstract | 第9-10页 |
| 第一章 绪论 | 第14-20页 |
| 1.1 研究背景和意义 | 第14-15页 |
| 1.2 国内外研究现状 | 第15-16页 |
| 1.2.1 无人驾驶系统研究现状 | 第15页 |
| 1.2.2 形式化验证方法应用研究现状 | 第15-16页 |
| 1.3 矿井机车无人驾驶系统概述 | 第16-18页 |
| 1.4 论文课题来源及研究内容和组织结构 | 第18-20页 |
| 1.4.1 课题来源 | 第18页 |
| 1.4.2 研究内容 | 第18页 |
| 1.4.3 组织结构 | 第18-20页 |
| 第二章 相关理论与工具介绍 | 第20-27页 |
| 2.1 时间自动机相关理论 | 第20-21页 |
| 2.1.1 时间自动机定义 | 第20页 |
| 2.1.2 时间自动机语义 | 第20-21页 |
| 2.1.3 时间自动机网络 | 第21页 |
| 2.2 时间自动机模型检测工具Uppaal | 第21-26页 |
| 2.2.1 Uppaal概述 | 第21-22页 |
| 2.2.2 Uppaal模板基本概念 | 第22-23页 |
| 2.2.3 Uppaal需求规约语言 | 第23-25页 |
| 2.2.4 基于Uppaal的模型检测过程 | 第25-26页 |
| 2.3 本章小结 | 第26-27页 |
| 第三章 矿井机车无人驾驶系统建模与验证方法 | 第27-34页 |
| 3.1 矿井机车运行过程分析 | 第27-29页 |
| 3.2 矿井机车无人驾驶系统总体设计 | 第29-31页 |
| 3.2.1 矿井机车自主驾驶原理 | 第29页 |
| 3.2.2 矿井机车无人驾驶系统数据交互设计 | 第29-30页 |
| 3.2.3 无人驾驶机车控制总体流程 | 第30-31页 |
| 3.3 矿井机车无人驾驶系统建模及验证方法 | 第31-33页 |
| 3.3.1 矿井机车无人驾驶系统建模原则 | 第31-32页 |
| 3.3.2 矿井机车无人驾驶系统建模及验证方法描述 | 第32-33页 |
| 3.4 本章小结 | 第33-34页 |
| 第四章 矿井机车自主驾驶过程建模与验证 | 第34-48页 |
| 4.1 自主驾驶过程验证需求 | 第34页 |
| 4.2 自主驾驶过程模型分解及构建 | 第34-44页 |
| 4.2.1 数据采集设备建模 | 第34-36页 |
| 4.2.2 自主驾驶控制流程建模 | 第36-43页 |
| 4.2.3 执行机构建模 | 第43-44页 |
| 4.3 模型仿真与验证 | 第44-46页 |
| 4.3.1 自主驾驶过程时间自动机网络模型 | 第44页 |
| 4.3.2 自主驾驶过程模型仿真 | 第44-45页 |
| 4.3.3 自主驾驶过程需求验证 | 第45-46页 |
| 4.4 本章小结 | 第46-48页 |
| 第五章 矿井机车遥控驾驶过程建模与验证 | 第48-59页 |
| 5.1 遥控驾驶过程模型分析 | 第48页 |
| 5.2 遥控驾驶过程验证需求 | 第48-49页 |
| 5.3 遥控驾驶控制过程模型分解及构建 | 第49-55页 |
| 5.3.1 网络数据传输时间自动机模型 | 第49-50页 |
| 5.3.2 遥控操作台模型 | 第50-53页 |
| 5.3.3 遥控驾驶员模型 | 第53-54页 |
| 5.3.4 机车控制器模型 | 第54-55页 |
| 5.4 模型仿真与验证 | 第55-58页 |
| 5.4.1 遥控驾驶过程时间自动机网络模型 | 第55-56页 |
| 5.4.2 遥控驾驶过程仿真 | 第56页 |
| 5.4.3 遥控驾驶过程验证 | 第56-58页 |
| 5.5 本章小结 | 第58-59页 |
| 第六章 总结与展望 | 第59-61页 |
| 6.1 总结 | 第59-60页 |
| 6.2 展望 | 第60-61页 |
| 参考文献 | 第61-64页 |
| 附录 | 第64-67页 |
| 攻读硕士学位期间的学术活动及成果情况 | 第67-69页 |