CPS系统信息物理协同验证技术研究
| 摘要 | 第4-6页 |
| Abstract | 第6-8页 |
| 第一章 绪论 | 第12-32页 |
| 1.1 选题背景及意义 | 第12-14页 |
| 1.2 一个典型的CPS应用及其实验平台 | 第14-17页 |
| 1.2.1 人造卫星姿态控制系统 | 第14-16页 |
| 1.2.2 实验平台--TableSat | 第16-17页 |
| 1.3 CPS相关研究工作 | 第17-20页 |
| 1.4 CPS验证技术相关研究工作 | 第20-26页 |
| 1.4.1 软硬件协同验证 | 第20-21页 |
| 1.4.2 混成系统验证 | 第21-22页 |
| 1.4.3 CPS协同验证 | 第22-26页 |
| 1.5 问题描述 | 第26-28页 |
| 1.6 论文的主要贡献 | 第28-29页 |
| 1.7 论文组织结构 | 第29-32页 |
| 第二章 CPS系统分析及协同验证框架 | 第32-56页 |
| 2.1 引言 | 第32页 |
| 2.2 迁移系统 | 第32-34页 |
| 2.3 CPS系统分析 | 第34-39页 |
| 2.3.1 CPS系统的体系结构分析 | 第34-35页 |
| 2.3.2 CPS系统任务的控制周期分析 | 第35-36页 |
| 2.3.3 CPS系统的开发流程分析 | 第36-38页 |
| 2.3.4 CPS系统的协同验证对象分析 | 第38-39页 |
| 2.4 源程序的形式化验证方法分析 | 第39-45页 |
| 2.4.1 基于定理证明技术的验证方法 | 第39-44页 |
| 2.4.2 基于模型检验技术的验证方法 | 第44-45页 |
| 2.5 CPS协同验证框架 | 第45-48页 |
| 2.6 CPS协同验证对象模型 | 第48-54页 |
| 2.6.1 验证对象模型的静态体系结构 | 第49-51页 |
| 2.6.2 验证对象模型的形式描述 | 第51-54页 |
| 2.7 本章小结 | 第54-56页 |
| 第三章 CPS形式化协同验证方法 | 第56-88页 |
| 3.1 引言 | 第56-58页 |
| 3.2 系统验证规约描述 | 第58-60页 |
| 3.2.1 线性时序逻辑 | 第58-59页 |
| 3.2.2 基于LTL的系统验证性质描述 | 第59-60页 |
| 3.3 系统形式化验证模型 | 第60-72页 |
| 3.3.1 控制应用程序的抽象模型 | 第60-64页 |
| 3.3.2 物理系统的抽象模型 | 第64-66页 |
| 3.3.3 逻辑交互模型 | 第66页 |
| 3.3.4 系统形式化验证模型 | 第66-70页 |
| 3.3.5 系统形式化验证模型的组装 | 第70-72页 |
| 3.4 协同验证算法 | 第72-79页 |
| 3.4.1 LTL模型检验算法 | 第72-75页 |
| 3.4.2 可达性分析 | 第75-76页 |
| 3.4.3 算法优化 | 第76-79页 |
| 3.5 CPS协同验证工具原型CO-VER | 第79-80页 |
| 3.6 实验及结果分析 | 第80-87页 |
| 3.6.1 温度自动控制系统 | 第80-83页 |
| 3.6.2 汽车巡航控制系统 | 第83-87页 |
| 3.7 本章小结 | 第87-88页 |
| 第四章 CPS协同仿真方法 | 第88-118页 |
| 4.1 引言 | 第88-89页 |
| 4.2 多领域协同仿真方法 | 第89-93页 |
| 4.2.1 多领域协同仿真 | 第89-90页 |
| 4.2.2 虚拟硬件环境QEMU | 第90-91页 |
| 4.2.3 MATLAB/Simulink | 第91-93页 |
| 4.3 CPS协同仿真框架 | 第93-96页 |
| 4.3.1 物理仿真模型 | 第94-95页 |
| 4.3.2 物理交互模型 | 第95-96页 |
| 4.4 时间同步机制 | 第96-103页 |
| 4.4.1 基于时钟理论的时间描述机制 | 第97-98页 |
| 4.4.2 计算模型的时间描述 | 第98-99页 |
| 4.4.3 物理仿真模型的时间描述 | 第99页 |
| 4.4.4 物理交互模型的时间描述 | 第99-101页 |
| 4.4.5 同步策略 | 第101-103页 |
| 4.5 CPS协同仿真工具原型CO-SIM | 第103-104页 |
| 4.6 实验及结果分析 | 第104-116页 |
| 4.6.1 TableSat的PID控制应用 | 第104-111页 |
| 4.6.2 汽车自动变速器控制系统 | 第111-116页 |
| 4.7 本章小结 | 第116-118页 |
| 第五章 CPS半形式化协同验证方法 | 第118-132页 |
| 5.1 引言 | 第118页 |
| 5.2 半形式化协同验证的算法 | 第118-120页 |
| 5.3 半形式化协同验证的实现 | 第120-121页 |
| 5.4 TABLESAT应用验证 | 第121-130页 |
| 5.4.1 TableSat设计与实现 | 第121-123页 |
| 5.4.2 TableSat协同验证 | 第123-130页 |
| 5.5 本章小结 | 第130-132页 |
| 第六章 总结与展望 | 第132-136页 |
| 6.1 本文工作的总结 | 第132-133页 |
| 6.2 未来工作的展望 | 第133-136页 |
| 参考文献 | 第136-149页 |
| 致谢 | 第149-150页 |
| 攻读博士学位期间发表的学术论文和参加科研情况 | 第150-152页 |
