基于内存和状态管理的模型检测方法
| 摘要 | 第1-6页 |
| ABSTRACT | 第6-11页 |
| 第一章 引言 | 第11-15页 |
| ·研究背景及意义 | 第11-12页 |
| ·课题的国内外研究状况 | 第12-13页 |
| ·论文的主要工作 | 第13-14页 |
| ·本文的组织结构 | 第14-15页 |
| 第二章 模型检测及相关技术 | 第15-30页 |
| ·线性时态逻辑 | 第15-20页 |
| ·LTL 的语法 | 第15-16页 |
| ·LTL 的语义 | 第16-18页 |
| ·LTL 公式之间的重要等价 | 第18-19页 |
| ·LTL 的适当连接词 | 第19-20页 |
| ·模型检测 | 第20-23页 |
| ·MC 概述 | 第20页 |
| ·MC 过程 | 第20-21页 |
| ·LTL 模型检测算法 | 第21-23页 |
| ·Büchi 自动机 | 第23-27页 |
| ·一般的 Büchi 自动机 | 第23-24页 |
| ·检测空集 | 第24-27页 |
| ·On-the-fly 模型检测 | 第27-29页 |
| ·小结 | 第29-30页 |
| 第三章 SPIN 结构分析及简介 | 第30-40页 |
| ·概述 | 第30-31页 |
| ·SPIN 的历史 | 第30-31页 |
| ·SPIN 的优点 | 第31页 |
| ·SPIN 的理论基础 | 第31-33页 |
| ·SPIN 的基本结构 | 第31-32页 |
| ·SPIN 的工作原理 | 第32-33页 |
| ·SPIN 的基本数据结构 | 第33-35页 |
| ·状态矢量 | 第33-35页 |
| ·DFS 堆栈 | 第35页 |
| ·已遍历的状态集合 | 第35页 |
| ·SPIN 的输入语言 | 第35-39页 |
| ·Promela 语言简介 | 第35-39页 |
| ·小结 | 第39-40页 |
| 第四章 算法描述和分析 | 第40-57页 |
| ·内存与状态管理技术 | 第40-47页 |
| ·固定内存管理技术 | 第40-44页 |
| ·动态内存管理技术 | 第44-47页 |
| ·基于动态内存和状态管理的路径搜索算法 | 第47-52页 |
| ·搜索反例路径 | 第47-50页 |
| ·反例的路径计算 | 第50页 |
| ·算法的正确性 | 第50-52页 |
| ·基于固定内存和状态管理的路径搜索算法 | 第52-55页 |
| ·路径的搜索 | 第52-54页 |
| ·计算反例路径 | 第54-55页 |
| ·算法正确性的证明 | 第55页 |
| ·小结 | 第55-57页 |
| 第五章 算法实现及实验 | 第57-74页 |
| ·算法实现 | 第57-67页 |
| ·开发环境 | 第58页 |
| ·数据结构介绍 | 第58-59页 |
| ·函数介绍及分析 | 第59-60页 |
| ·状态处理 | 第60页 |
| ·设计实现 | 第60-67页 |
| ·实验 | 第67-72页 |
| ·设计实验 | 第67-68页 |
| ·Bakery(8),P3 | 第68-70页 |
| ·Peterson(4),P4 | 第70-71页 |
| ·Elevator2(16),P4 | 第71-72页 |
| ·小结 | 第72-74页 |
| 第六章 结论 | 第74-75页 |
| 致谢 | 第75-76页 |
| 参考文献 | 第76-78页 |
