信息流图分割算法的设计与信息流的PVS实现
| 摘要 | 第1-6页 |
| Abstract | 第6-9页 |
| 第一章 引言 | 第9-19页 |
| ·隐通道的提出 | 第9-10页 |
| ·关于信息流分析的相关概念 | 第10-17页 |
| ·信息传导机制 | 第11-14页 |
| ·信息流图 | 第14-16页 |
| ·原型验证系统 | 第16-17页 |
| ·本文主要工作和组织结构 | 第17-19页 |
| 第二章 信息流图的分割算法 | 第19-37页 |
| ·问题的提出 | 第19-21页 |
| ·相关定义、定理及符号 | 第21-26页 |
| ·符号约束 | 第21-22页 |
| ·相关定义 | 第22页 |
| ·相关定理及证明 | 第22-26页 |
| ·信息流图分割成信息流森林的算法 | 第26-29页 |
| ·算法的自然语言描述 | 第26-27页 |
| ·算法的伪代码表达 | 第27-29页 |
| ·算法性质及理论证明 | 第29-33页 |
| ·算法第一性质及证明 | 第29页 |
| ·算法第二性质及证明 | 第29-31页 |
| ·算法第三性质及证明 | 第31-33页 |
| ·实例分析 | 第33-35页 |
| ·结论及分析 | 第35-37页 |
| 第三章 PVS规约信息流及规约的相关定理 | 第37-47页 |
| ·PVS原型验证系统及简述 | 第37-39页 |
| ·信息流的PVS规约 | 第39-42页 |
| ·信息流的抽象 | 第39-40页 |
| ·规约数据结构 | 第40-41页 |
| ·规约转换模块 | 第41页 |
| ·规约功能模块 | 第41-42页 |
| ·界定组态 | 第42页 |
| ·信息流规约的相关定理 | 第42-45页 |
| ·规约完整性定理 | 第43页 |
| ·隐通道鉴别定理 | 第43-45页 |
| ·结果不变性定理 | 第45页 |
| ·本章小结 | 第45-47页 |
| 第四章 实例分析 | 第47-63页 |
| ·信息流图的生成 | 第47-50页 |
| ·信息流图分解成信息流森林 | 第50-56页 |
| ·信息流森林的PVS验证 | 第56-63页 |
| 第五章 结论 | 第63-65页 |
| 参考文献 | 第65-68页 |
| 附录 | 第68-76页 |
| 附录1 | 第68-71页 |
| 附录2 | 第71-76页 |
| 致谢 | 第76-77页 |
| 发表文章 | 第77页 |
