混合系统的形式验证方法及其应用
| 第一章 绪论 | 第1-19页 |
| ·混合系统简介 | 第12-15页 |
| ·混合系统的概念 | 第12页 |
| ·混合系统的典型例子 | 第12-14页 |
| ·混合系统研究的意义与历史 | 第14-15页 |
| ·混合系统研究的主要问题 | 第15-16页 |
| ·混合系统的建模 | 第15页 |
| ·混合系统的分析 | 第15-16页 |
| ·混合系统的综合 | 第16页 |
| ·混合系统的形式验证 | 第16-17页 |
| ·混合系统形式验证研究的意义 | 第16-17页 |
| ·混合系统形式验证研究的现状 | 第17页 |
| ·本文的研究内容与结构 | 第17-19页 |
| 第二章 混合系统的形式验证原理 | 第19-27页 |
| ·基于自动机的混合系统模型 | 第19-23页 |
| ·混合自动机定义 | 第19-20页 |
| ·线性混合系统 | 第20-21页 |
| ·线性混合自动机 | 第21页 |
| ·混合自动机实例 | 第21-23页 |
| ·两容水箱系统 | 第21-22页 |
| ·水位监控系统 | 第22-23页 |
| ·混合系统的可达集计算 | 第23-24页 |
| ·收敛近似方法 | 第23页 |
| ·过近似方法 | 第23-24页 |
| ·商迁移系统与仿真对 | 第24-25页 |
| ·迁移系统与商迁移系统 | 第24页 |
| ·仿真对 | 第24-25页 |
| ·混合系统形式验证的可决策性 | 第25页 |
| ·混合系统形式验证的过程 | 第25-27页 |
| 第三章 基于模型检验的验证工具 | 第27-32页 |
| ·各种验证工具及其算法的简介 | 第27-30页 |
| ·Hytech | 第27-28页 |
| ·CheckMate | 第28-29页 |
| ·Verdict | 第29页 |
| ·d/dt | 第29-30页 |
| ·各种验证工具的比较 | 第30-32页 |
| 第四章 基于流管道和切换面划分的形式验证方法 | 第32-49页 |
| ·多面体不变集混合自动机 | 第32-33页 |
| ·离散抽象迁移系统 | 第33页 |
| ·有限状态近似商迁移系统的计算 | 第33-38页 |
| ·迁移系统仿真对的计算 | 第34页 |
| ·有限状态近似商迁移系统 | 第34-35页 |
| ·阈值切换面划分与迁移系统状态的确定 | 第35-36页 |
| ·流管道计算与迁移系统状态之间迁移关系的确定 | 第36-38页 |
| ·线性连续动态的迁移关系计算的改进方法 | 第38-40页 |
| ·模型检验 | 第40-45页 |
| ·计算树逻辑 | 第40-42页 |
| ·基于受限计算树逻辑的规范描述 | 第42页 |
| ·标记模型检验 | 第42-44页 |
| ·基于固定点的显示模型检验 | 第44-45页 |
| ·不可决策性与重新划分 | 第45-46页 |
| ·化工过程验证实例 | 第46-49页 |
| 第五章 倒立摆模型的形式验证 | 第49-57页 |
| ·倒立摆模型与规范要求 | 第49-50页 |
| ·CheckMate模型 | 第50-55页 |
| ·验证工具CheckMate | 第50-52页 |
| ·系统描述 | 第52-55页 |
| ·规范描述 | 第55页 |
| ·验证结果 | 第55-57页 |
| 第六章 总结与展望 | 第57-59页 |
| 参考文献 | 第59-62页 |
