与测试相结合的系统安全性验证技术研究
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-7页 |
| 目录 | 第7-10页 |
| 第一章 绪论 | 第10-18页 |
| ·引言 | 第10-11页 |
| ·形式化验证技术 | 第11-15页 |
| ·验证技术的研究现状 | 第11-12页 |
| ·模型检测 | 第12-13页 |
| ·验证技术面临的主要问题和优化技术 | 第13-15页 |
| ·测试技术 | 第15-16页 |
| ·软件测试、协议测试 | 第15页 |
| ·测试的缺陷与发展 | 第15-16页 |
| ·测试与验证的结合 | 第16页 |
| ·主要内容和贡献 | 第16-17页 |
| ·论文结构 | 第17-18页 |
| 第二章 程序模型检测和IOSTS系统 | 第18-28页 |
| ·程序模型检测技术介绍 | 第18-19页 |
| ·相关工作介绍 | 第19-21页 |
| ·程序模型检测的主要工具和方法 | 第19-21页 |
| ·程序模型检测的两阶段框架 | 第21页 |
| ·SPIN/PROMELA概述 | 第21-22页 |
| ·C程序模型检测工具COPPER简介 | 第22-25页 |
| ·测试与验证的模型 | 第25-27页 |
| ·IOSTS模型的定义 | 第25-26页 |
| ·IOSTS上的基本操作 | 第26-27页 |
| ·本章小结 | 第27-28页 |
| 第三章 IOCO一致性所存在的问题和系统安全性 | 第28-36页 |
| ·IOCO一致性 | 第28-34页 |
| ·ioco一致性的概念 | 第28-30页 |
| ·ioco一致性的两类缺陷 | 第30-34页 |
| ·系统安全性 | 第34-35页 |
| ·问题回顾 | 第34页 |
| ·违背安全性的迹以及系统违背安全性的定义 | 第34-35页 |
| ·本章小结 | 第35-36页 |
| 第四章 SDR算法与应用实例介绍 | 第36-53页 |
| ·将COPPER的输出转化为IOSTS表示 | 第36-39页 |
| ·安全性缺陷补救算法SDR | 第39-40页 |
| ·使用SDR算法弥补IOCO一致性缺陷 | 第40-48页 |
| ·工作原理 | 第40-42页 |
| ·技术方法 | 第42-48页 |
| ·使用SDR算法对ATM系统进行安全性验证实例 | 第48-52页 |
| ·本章小结 | 第52-53页 |
| 第五章 结论和进一步工作 | 第53-55页 |
| ·论文总结 | 第53页 |
| ·进一步工作 | 第53-55页 |
| 参考文献 | 第55-58页 |
| 致谢 | 第58-59页 |
| 附:攻读硕士期间参加的研究项目 | 第59页 |
