| 第一章 绪论 | 第1-12页 |
| ·研究背景 | 第9-10页 |
| ·研究现状 | 第10页 |
| ·主要的研究工作 | 第10-11页 |
| ·本文的组织结构 | 第11-12页 |
| 第二章 形式化方法 | 第12-18页 |
| ·形式化方法的基本概念和发展历史 | 第12-14页 |
| ·形式化方法的局限性 | 第14-15页 |
| ·形式化方法不能代替传统的方法 | 第14-15页 |
| ·规范的正确性 | 第15页 |
| ·证明的正确性 | 第15页 |
| ·模型的准确性 | 第15页 |
| ·形式化方法的分类 | 第15-18页 |
| ·系统规范 | 第15-16页 |
| ·形式化验证 | 第16-18页 |
| 第三章 模型检测的基本理论 | 第18-33页 |
| ·Computation tree logics(CTL*)计算树逻辑 | 第18-21页 |
| ·Branch Time logics分支时态逻辑 | 第21-24页 |
| ·二叉判定图(Binary Decision Diagram) | 第24-29页 |
| ·布尔函数和二叉判定图 | 第24-27页 |
| ·符号模型检测(Symbolic Model Checking) | 第27-29页 |
| ·硬件系统验证概要 | 第29-30页 |
| ·抽象技术 | 第30-33页 |
| 第四章 模型检测工具SPIN | 第33-43页 |
| ·Spin简介 | 第33页 |
| ·Spin的基本架构 | 第33-34页 |
| ·线性时态逻辑 | 第34-36页 |
| ·Bü chi自动机 | 第36-39页 |
| ·Promela语言 | 第39-43页 |
| ·Hello world程序 | 第40页 |
| ·Promela语言简介 | 第40-43页 |
| 第五章 验证FAIRILSE ATM交换机行为 | 第43-54页 |
| ·FAIRILSE ATM的硬件组成 | 第43-45页 |
| ·FAIRILSE ATM交换机行为的抽象描述 | 第45-47页 |
| ·FAIRILSE ATM交换机行为建模 | 第47-54页 |
| ·建模的一般方法 | 第48页 |
| ·建立AIM交换机的一个最小模型 | 第48-54页 |
| 第六章 总结与展望 | 第54-55页 |
| 参考文献 | 第55-58页 |
| 致谢 | 第58页 |
