基于PVS的自稳定算法形式化分析
| 摘要 | 第1-7页 |
| ABSTRACT | 第7-11页 |
| 第一章 绪论 | 第11-18页 |
| ·引言 | 第11-12页 |
| ·形式化分析方法概述 | 第12-16页 |
| ·形式化方法的定义 | 第12页 |
| ·形式化方法的发展 | 第12-13页 |
| ·形式化方法的研究内容 | 第13-15页 |
| ·形式化方法的分类 | 第15-16页 |
| ·研究内容与成果 | 第16页 |
| ·本文结构 | 第16-18页 |
| 第二章 自稳定算法和原型验证系统 | 第18-25页 |
| ·自稳定算法 | 第18-22页 |
| ·分布式系统 | 第18-20页 |
| ·分布式算法 | 第20页 |
| ·自稳定性的定义 | 第20页 |
| ·暂时性错误 | 第20-21页 |
| ·自稳定系统 | 第21-22页 |
| ·原型验证系统 | 第22-24页 |
| ·PVS 的历史和作用 | 第22页 |
| ·PVS 的规约语言 | 第22-23页 |
| ·PVS 的定理证明器 | 第23-24页 |
| ·本章小结 | 第24-25页 |
| 第三章 自稳定算法的设计与验证 | 第25-38页 |
| ·自稳定算法的提出 | 第25-27页 |
| ·经典Dijkstra 互斥算法 | 第27-29页 |
| ·自稳定算法的设计 | 第29-33页 |
| ·中央控制系统的作用 | 第30-31页 |
| ·系统网络拓扑结构 | 第31页 |
| ·系统进程状态数 | 第31-32页 |
| ·算法的时间和空间复杂度 | 第32页 |
| ·算法的对称性和随机性 | 第32-33页 |
| ·自稳定算法的验证方法 | 第33-36页 |
| ·数学方法 | 第33-34页 |
| ·形式化验证方法 | 第34-36页 |
| ·机械验证和数学验证的比较 | 第36页 |
| ·本章小结 | 第36-38页 |
| 第四章 形式化建模与实例分析 | 第38-56页 |
| ·自稳定算法的数学验证 | 第38-43页 |
| ·算法的基本定义和描述 | 第38-39页 |
| ·算法的数学验证 | 第39-43页 |
| ·自稳定算法的形式化验证 | 第43-54页 |
| ·PVS 的语法和语义 | 第43-45页 |
| ·算法的基本描述 | 第45-46页 |
| ·算法的基本性质 | 第46-47页 |
| ·算法的形式化建模 | 第47-52页 |
| ·算法的自动化验证 | 第52-54页 |
| ·本章小结 | 第54-56页 |
| 第五章 全文总结和展望 | 第56-59页 |
| ·工作总结 | 第56-57页 |
| ·未来工作和展望 | 第57-59页 |
| 参考文献 | 第59-62页 |
| 附录 | 第62-67页 |
| 附录I：自稳定算法的PVS 形式化描述 | 第62-67页 |
| 致谢 | 第67-69页 |
| 攻读硕士学位期间发表的论文 | 第69-71页 |
