基于可达集过近似的混合系统验证方法
| 摘要 | 第1-6页 |
| ABSTRACT | 第6-13页 |
| 第一章 绪论 | 第13-18页 |
| ·混合系统的概念和特点 | 第13-14页 |
| ·混合系统的发展概况 | 第14页 |
| ·混合系统的典型例子 | 第14-15页 |
| ·双容水箱系统 | 第14-15页 |
| ·房间温度控制系统 | 第15页 |
| ·混合系统的形式化验证 | 第15-17页 |
| ·系统仿真与形式化验证 | 第16页 |
| ·混合系统的形式化验证的发展 | 第16页 |
| ·基于模型检验的混合系统形式化验证工具 | 第16-17页 |
| ·本文的主要内容 | 第17-18页 |
| 第二章 混合系统验证中的基本概念 | 第18-24页 |
| ·迁移系统与商迁移系统 | 第18-19页 |
| ·迁移系统 | 第18页 |
| ·商迁移系统 | 第18页 |
| ·离散抽象迁移系统 | 第18-19页 |
| ·仿真与仿真对 | 第19-20页 |
| ·混合系统形式验证的可决策性 | 第20页 |
| ·模型检验技术 | 第20-24页 |
| ·计算树逻辑CTL | 第21-23页 |
| ·计算树逻辑的组成 | 第21-22页 |
| ·计算树逻辑实例 | 第22-23页 |
| ·基于动作的时序逻辑ACTL | 第23-24页 |
| 第三章 混合系统的形式化验证原理 | 第24-38页 |
| ·混合系统形式化验证的流程 | 第24-25页 |
| ·混合系统建模 | 第25-28页 |
| ·混合自动机 | 第25-26页 |
| ·混合自动机建模实例 | 第26-28页 |
| ·双容水箱系统 | 第26-27页 |
| ·房间温度控制系统 | 第27-28页 |
| ·初始划分 | 第28-30页 |
| ·初始划分的必要性 | 第28-29页 |
| ·切换面的分类 | 第29页 |
| ·初始划分的标准 | 第29-30页 |
| ·可达集近似 | 第30-36页 |
| ·流管道计算的原理 | 第30-32页 |
| ·可达集的表示法和算法的选择 | 第30-32页 |
| ·流管道的分段近似 | 第32页 |
| ·流管道计算的方法 | 第32-34页 |
| ·流管道的过近似算法 | 第33页 |
| ·线性系统的仿射 | 第33-34页 |
| ·不变集内的流管道计算 | 第34-35页 |
| ·下一个不变集的初始状态的确定 | 第35-36页 |
| ·商迁移系统迁移关系的确定 | 第36页 |
| ·商迁移系统的模型检验 | 第36页 |
| ·商迁移系统的细划分 | 第36-38页 |
| ·细划分的定义 | 第37页 |
| ·细划分的原则 | 第37-38页 |
| 第四章 一类混合系统迁移关系的简化算法 | 第38-45页 |
| ·问题的提出 | 第38页 |
| ·结论和证明 | 第38-40页 |
| ·简化算法 | 第40页 |
| ·算法的程序框图 | 第40-43页 |
| ·商迁移系统迁移关系简化算法的程序框图 | 第41页 |
| ·流管道过近似的程序框图 | 第41-42页 |
| ·仿射计算的程序框图 | 第42-43页 |
| ·算法保守性的讨论 | 第43-45页 |
| ·保守性讨论一 | 第43页 |
| ·保守性讨论二 | 第43-45页 |
| 第五章 验证实例 | 第45-59页 |
| ·分段线性系统 | 第45-49页 |
| ·问题描述 | 第45-46页 |
| ·建立混合自动机模型 | 第46-47页 |
| ·验证规范 | 第47页 |
| ·可达集近似计算 | 第47-49页 |
| ·系统验证 | 第49页 |
| ·小球系统 | 第49-58页 |
| ·问题描述 | 第49-51页 |
| ·建立混合自动机模型 | 第51页 |
| ·验证过程 | 第51-54页 |
| ·用可达集近似的方法计算迁移关系 | 第52页 |
| ·用顶点仿真与可达集近似结合的方法计算迁移关系 | 第52-54页 |
| ·小球系统的商迁移系统 | 第54页 |
| ·对比与分析 | 第54-58页 |
| ·计算量的对比分析 | 第54-55页 |
| ·保守性的对比分析 | 第55-58页 |
| ·结论 | 第58-59页 |
| 第六章 总结与展望 | 第59-61页 |
| ·本文总结 | 第59-60页 |
| ·后续研究工作的建议 | 第60-61页 |
| 参考文献 | 第61-64页 |
