基于SMT的实时系统可诊断性研究
| 摘要 | 第6-8页 |
| ABSTRACT | 第8-9页 |
| 符号对照表 | 第12-13页 |
| 缩略语对照表 | 第13-16页 |
| 第一章 绪论 | 第16-24页 |
| 1.1 研究背景与现状 | 第17-21页 |
| 1.1.1 基于模型诊断 | 第17-18页 |
| 1.1.2 可诊断性研究 | 第18-21页 |
| 1.2 本文主要工作 | 第21-22页 |
| 1.3 本文组织结构 | 第22-24页 |
| 第二章 可满足性模理论下的逻辑验证 | 第24-32页 |
| 2.1 SAT问题及逻辑验证 | 第24-27页 |
| 2.1.1 SAT背景知识 | 第24-25页 |
| 2.1.2 SAT问题验证算法 | 第25-27页 |
| 2.2 SMT问题及逻辑验证 | 第27-32页 |
| 2.2.1 SMT背景知识 | 第27-29页 |
| 2.2.2 SMT求解器 | 第29-32页 |
| 第三章 基于时间自动机的可诊断性检测 | 第32-42页 |
| 3.1 基于FSM的可诊断性判定 | 第32-37页 |
| 3.2 基于TA的可诊断性判定 | 第37-40页 |
| 3.3 本章小结 | 第40-42页 |
| 第四章 基于SMT的有界可诊断性检测 | 第42-54页 |
| 4.1 基于SMT的时间自动机编码 | 第42-43页 |
| 4.2 基于SMT有界可诊断性编码 | 第43-52页 |
| 4.2.1 有界可诊断性编码规则 | 第44-50页 |
| 4.2.2 有界可诊断性检验 | 第50-52页 |
| 4.3 本章小结 | 第52-54页 |
| 第五章 实验及分析 | 第54-64页 |
| 5.1 HVAC系统实验 | 第54-62页 |
| 5.1.2 实验一 | 第55-58页 |
| 5.1.3 实验二 | 第58-61页 |
| 5.1.4 实验三 | 第61-62页 |
| 5.2 实验结果分析 | 第62-64页 |
| 第六章 结论与展望 | 第64-66页 |
| 参考文献 | 第66-70页 |
| 致谢 | 第70-72页 |
| 作者简介 | 第72-73页 |
