基于D3S的在线程序分析技术的研究
| 摘要 | 第1-7页 |
| ABSTRACT | 第7-13页 |
| 第一章 绪论 | 第13-20页 |
| ·引言 | 第13-15页 |
| ·相关工作 | 第15-19页 |
| ·谓词检测技术 | 第15-16页 |
| ·代码级模型检测技术 | 第16-17页 |
| ·基于日志的调试技术 | 第17-18页 |
| ·模型检测技术简介 | 第18-19页 |
| ·关于本文 | 第19-20页 |
| ·研究目标 | 第19-20页 |
| ·章节安排 | 第20页 |
| 第二章 监控系统的理论模型 | 第20-42页 |
| ·分布式系统的全局状态 | 第21-25页 |
| ·LAMPORT 时间戳 | 第21-24页 |
| ·带全局时间戳的全局状态 | 第24-25页 |
| ·有限路径LTL | 第25-29页 |
| ·线性时态逻辑LTL | 第26-27页 |
| ·有限路径LTL 语法和语义 | 第27-28页 |
| ·时态性质 | 第28-29页 |
| ·有限自动机与有限路径LTL | 第29-38页 |
| ·GENERAL BüCHI 自动机和LGBA | 第30页 |
| ·LTL 与LGBA | 第30-34页 |
| ·LTL 与有限自动机模型 | 第34-38页 |
| ·监控系统有限自动机模型的正确性证明 | 第38-41页 |
| ·本章小结 | 第41-42页 |
| 第三章 监控系统的系统框架与实现 | 第42-72页 |
| ·监控系统的系统架构 | 第42-44页 |
| ·状态发送器概述 | 第43页 |
| ·LTL 引擎概述 | 第43-44页 |
| ·二进制注入技术 | 第44-46页 |
| ·状态发送器的实现 | 第46-52页 |
| ·数据结构 | 第47-49页 |
| ·状态发送器的通用模板 | 第49-52页 |
| ·LTL 引擎的实现 | 第52-66页 |
| ·模型检测工具SPIN 概述 | 第52-54页 |
| ·LTL 验证引擎的框架 | 第54-55页 |
| ·LTL 验证引擎的接口 | 第55-56页 |
| ·LTL 公式转换器 | 第56-64页 |
| ·有限路径LTL 验证器 | 第64-66页 |
| ·监控系统的应用案例 | 第66-70页 |
| ·哲学家就餐问题 | 第66-67页 |
| ·监控系统应用 | 第67-70页 |
| ·本章小结 | 第70-72页 |
| 第四章 案例分析 | 第72-80页 |
| ·PAXOS 协议和一致性 | 第72页 |
| ·PAXOS 协议简介 | 第72-74页 |
| ·案例分析 | 第74-78页 |
| ·PAXOS 协议优化 | 第74-75页 |
| ·协议的时态特性以及系统产生的活锁 | 第75-78页 |
| ·性能开销 | 第78-79页 |
| ·本章小结 | 第79-80页 |
| 第五章 结论 | 第80-82页 |
| ·全文总结 | 第80-81页 |
| ·未来工作 | 第81-82页 |
| 参考文献 | 第82-85页 |
| 致谢 | 第85-86页 |
| 攻读硕士期间已发表的论文 | 第86页 |
