| 摘要 | 第1-5页 |
| Abstract | 第5-8页 |
| 第1章 引言 | 第8-11页 |
| ·研究背景 | 第8-9页 |
| ·研究内容 | 第9-10页 |
| ·本文结构 | 第10-11页 |
| 第2章 模型检测及相关技术 | 第11-16页 |
| ·模型检测及相关技术 | 第11-13页 |
| ·简述 | 第11页 |
| ·形式化方法概述 | 第11-12页 |
| ·模型检测基本原理 | 第12-13页 |
| ·状态爆炸问题 | 第13-15页 |
| ·产生的原因 | 第13-14页 |
| ·减少状态爆炸的技术 | 第14-15页 |
| ·本章小结 | 第15-16页 |
| 第3章 NuSMV及其支持的时态逻辑 | 第16-23页 |
| ·概述 | 第16页 |
| ·NuSMV系统结构 | 第16-18页 |
| ·时态逻辑(Temporal Logic) | 第18-22页 |
| ·计算树逻辑CTL(Computation Tree Logic) | 第19-20页 |
| ·线性时态逻辑Linear temporal logic(LTL) | 第20-21页 |
| ·PSL | 第21-22页 |
| ·本章小结 | 第22-23页 |
| 第4章 PCI总线协议中设备和仲裁器建模 | 第23-33页 |
| ·PCI总线信号和命令 | 第23-25页 |
| ·PCI总线信号 | 第23-24页 |
| ·PCI总线命令 | 第24-25页 |
| ·PCI总线信号和命令建模 | 第25-26页 |
| ·主从设备读/写交易(transactions) | 第26-29页 |
| ·主从设备读/写交易(transactions)建模 | 第29-31页 |
| ·设备调度策略的建模 | 第31-32页 |
| ·本章小结 | 第32-33页 |
| 第5章 PCI总线协议中设备和仲裁器具体实现 | 第33-51页 |
| ·各个子模块的实现 | 第33-43页 |
| ·arbitrator实现 | 第33-39页 |
| ·总线主设备实现 | 第39-43页 |
| ·主模块(MODUAL main)的实现 | 第43-47页 |
| ·实验结果及分析 | 第47-49页 |
| ·本章小结 | 第49-51页 |
| 第6章 全文总结 | 第51-52页 |
| 参考文献 | 第52-55页 |
| 致谢 | 第55-56页 |
| 攻读硕士学位期间发表的学术论文 | 第56页 |
