Hybrid Event-B：信息物理融合系统的建模及精化方法
| 摘要 | 第5-7页 |
| ABSTRACT | 第7-9页 |
| 第一章 绪论 | 第14-30页 |
| 1.1 信息物理融合系统 | 第14-17页 |
| 1.2 精化开发信息物理融合系统 | 第17-20页 |
| 1.3 研究方案与创新点 | 第20-23页 |
| 1.4 相关工作 | 第23-28页 |
| 1.4.1 Event-B的扩展研究 | 第23-24页 |
| 1.4.2 微分不变量生成研究 | 第24-25页 |
| 1.4.3 微分不变量验证工具 | 第25页 |
| 1.4.4 混成系统精化研究 | 第25-26页 |
| 1.4.5 相关工具介绍 | 第26-28页 |
| 1.5 论文结构 | 第28-30页 |
| 第二章 Hybrid Event-B建模语言 | 第30-42页 |
| 2.1 微分动力系统 | 第30-31页 |
| 2.2 混成协作机制 | 第31-33页 |
| 2.3 Hybrid Event-B事件 | 第33-38页 |
| 2.3.1 事件结构 | 第33-35页 |
| 2.3.2 离散事件 | 第35页 |
| 2.3.3 微分事件 | 第35-37页 |
| 2.3.4 事件协作机制 | 第37-38页 |
| 2.4 Hybrid Event-B建模案例 | 第38-40页 |
| 2.5 本章小结 | 第40-42页 |
| 第三章 Hybrid Event-B的证明义务 | 第42-52页 |
| 3.1 证明义务 | 第42-43页 |
| 3.2 不变量保持证明义务 | 第43-45页 |
| 3.3 可靠性证明义务 | 第45-46页 |
| 3.4 精化证明义务 | 第46-51页 |
| 3.5 本章小结 | 第51-52页 |
| 第四章 证明义务的证明 | 第52-60页 |
| 4.1 归纳证明 | 第52-55页 |
| 4.1.1 归纳不变量 | 第52页 |
| 4.1.2 微分不变量 | 第52-55页 |
| 4.2 证明义务规则的证明 | 第55-58页 |
| 4.3 本章小结 | 第58-60页 |
| 第五章 Rodin工具扩展 | 第60-70页 |
| 5.1 扩展方案 | 第60-61页 |
| 5.2 建模能力扩展 | 第61-64页 |
| 5.3 定理证明器整合 | 第64-68页 |
| 5.3.1 Rodin的证明机制 | 第64-65页 |
| 5.3.2 微分事件证明义务证明 | 第65-68页 |
| 5.4 本章小结 | 第68-70页 |
| 第六章 应用案例-轨道交通控制系统 | 第70-90页 |
| 6.1 铁道岔口控制子系统 | 第70-78页 |
| 6.1.1 初始模型 | 第70-75页 |
| 6.1.2 精化模型 | 第75-78页 |
| 6.2 火车安全距离控制子系统 | 第78-88页 |
| 6.2.1 初始模型 | 第79-83页 |
| 6.2.2 精化模型 | 第83-88页 |
| 6.3 本章小结 | 第88-90页 |
| 第七章 总结与展望 | 第90-92页 |
| 7.1 总结 | 第90-91页 |
| 7.2 展望 | 第91-92页 |
| 参考文献 | 第92-102页 |
| 攻读博士学位期间发表的论文 | 第102-104页 |
| 攻读博士学位期间参加的课题 | 第104-106页 |
| 致谢 | 第106页 |
