SPIN模型检测的形式化分析机理研究及应用
| 摘要 | 第1-4页 |
| ABSTRACT | 第4-7页 |
| 第1章 绪论 | 第7-10页 |
| ·研究背景 | 第7-8页 |
| ·研究内容 | 第8-9页 |
| ·本文结构 | 第9-10页 |
| 第2章 模型检测及相关技术 | 第10-17页 |
| ·模型检测技术 | 第10-14页 |
| ·简述 | 第10-12页 |
| ·状态爆炸问题 | 第12-14页 |
| ·常见模型检测器的应用 | 第14-17页 |
| ·硬件和协议验证 | 第14-15页 |
| ·软件验证 | 第15-17页 |
| 第3章 SPIN模型检测的形式化分析机理 | 第17-30页 |
| ·概述 | 第17-18页 |
| ·SPIN的发展历史 | 第17-18页 |
| ·SPIN的特点 | 第18页 |
| ·SPIN的理论基础 | 第18-20页 |
| ·SPIN的基本结构 | 第18-19页 |
| ·SPIN的工作原理 | 第19-20页 |
| ·SPIN的基本数据结构及实例解析 | 第20-25页 |
| ·状态矢量(State vector) | 第20-21页 |
| ·Depth-first stack | 第21-24页 |
| ·Seen state set | 第24-25页 |
| ·线性时序逻辑LTL | 第25-27页 |
| ·Stutter不变性 | 第25页 |
| ·线性时序逻辑LTL语法 | 第25-26页 |
| ·线性时序逻辑LTL语义 | 第26页 |
| ·时态逻辑对系统性质的描述 | 第26-27页 |
| ·有限自动机 | 第27-28页 |
| ·从线性时序逻辑到有限自动机的转换 | 第28-30页 |
| 第4章 SPIN的建模语言PROMELA | 第30-45页 |
| ·进程说明 | 第30-32页 |
| ·数据类型 | 第32-33页 |
| ·消息通道 | 第33-36页 |
| ·可执行性 | 第36页 |
| ·流向控制 | 第36-40页 |
| ·断言类型 | 第40-42页 |
| ·其他特点 | 第42-43页 |
| ·实例分析 | 第43-45页 |
| 第5章 SPIN模型检测求解离散化问题 | 第45-65页 |
| ·一般方法 | 第45-50页 |
| ·实例一:士兵过桥问题 | 第45-50页 |
| ·分析离散化问题算法 | 第50页 |
| ·改进方法 | 第50-59页 |
| ·SPIN中嵌入C代码的原语说明 | 第51-54页 |
| ·结合分支界限技术分析实例一 | 第54-55页 |
| ·实例二:个性化卡片问题 | 第55-59页 |
| ·启发式方法优化模型 | 第59-64页 |
| ·深度优先搜索算法 | 第59页 |
| ·静态分析方法 | 第59-63页 |
| ·动态分析方法 | 第63-64页 |
| ·小结 | 第64-65页 |
| 第6章 结论与展望 | 第65-67页 |
| ·结论 | 第65页 |
| ·展望 | 第65-67页 |
| 致谢 | 第67-68页 |
| 参考文献 | 第68-72页 |
| 攻读学位期间的研究成果 | 第72页 |
