| 摘要 | 第1-7页 |
| Abstract | 第7-11页 |
| 第一章 绪论 | 第11-20页 |
| ·研究背景 | 第11-16页 |
| ·物联网和信息物理融合系统 | 第11-12页 |
| ·混成系统 | 第12-16页 |
| ·混成系统定义 | 第12-13页 |
| ·混成系统案例 | 第13-16页 |
| ·国内外研究现状 | 第16-17页 |
| ·研究内容和方法 | 第17-18页 |
| ·文章结构 | 第18-19页 |
| ·本章小结 | 第19-20页 |
| 第二章 微分动态逻辑对CPS的建模 | 第20-34页 |
| ·概述 | 第20-21页 |
| ·混成程序 | 第21-22页 |
| ·混成程序介绍 | 第21页 |
| ·混成程序的语法语义 | 第21-22页 |
| ·dL模型在形式化验证中的优势 | 第22-23页 |
| ·微分动态逻辑的推理演算法则 | 第23-29页 |
| ·铁路道口控制系统分析与建模 | 第29-33页 |
| ·铁路道口控制系统分析 | 第29-30页 |
| ·铁路道口控制系统建模 | 第30-33页 |
| ·本章小结 | 第33-34页 |
| 第三章 结构分析与设计语言对CPS的建模 | 第34-43页 |
| ·结构设计与分析语言介绍 | 第34-36页 |
| ·AADL概念 | 第34-35页 |
| ·AADL组件 | 第35-36页 |
| ·温度无线传感器网络模型 | 第36-42页 |
| ·温度无线传感器网络 | 第36-37页 |
| ·模型的建立 | 第37-42页 |
| ·本章小结 | 第42-43页 |
| 第四章 时钟理论对CPS的建模 | 第43-50页 |
| ·时钟理论的基本概念 | 第43-46页 |
| ·时钟理论的建模 | 第46-49页 |
| ·温度控制系统的时钟理论建模 | 第46-47页 |
| ·铁路道口控制的时钟理论建模 | 第47-49页 |
| ·本章小结 | 第49-50页 |
| 第五章 建模与验证的工具 | 第50-56页 |
| ·基于微分动态逻辑模型的工具KeYmaera | 第50页 |
| ·基于KeYmaera的性质验证 | 第50-53页 |
| ·AADL建模工具 | 第53-55页 |
| ·本章小结 | 第55-56页 |
| 第六章 总结与展望 | 第56-58页 |
| ·总结 | 第56-57页 |
| ·展望 | 第57-58页 |
| 附录A | 第58-61页 |
| A.1 火车道口控制系统安全性验证的KeYmaera程序 | 第58-60页 |
| A.2 AADL文本形式建模代码 | 第60-61页 |
| 参考文献 | 第61-65页 |
| 攻读硕士学位期间发表论文和参与科研项目情况 | 第65-66页 |
| 致谢 | 第66页 |