基于SPIN的协议的形式化分析和验证

摘要	第1-6页
Abstracts	第6-7页
第一章 绪论	第7-10页
·背景	第7-8页
·形式化方法	第7页
·协议工程	第7-8页
·研究目的	第8-9页
·相关工作	第9页
·本文组织结构	第9-10页
第二章 理论背景	第10-25页
·模型检测理论基础	第10-15页
·线性时态逻辑	第10-12页
·有穷自动机	第12-13页
·基本算法	第13-15页
·模型检测工具SPIN	第15-25页
·Spin简介	第15-16页
·Promela语言	第16-25页
第三章 基于SPIN的WTP协议的形式化	第25-52页
·协议描述	第25-34页
·协议环境	第25-26页
·事务层服务	第26-29页
·事务层协议	第29-30页
·协议特性	第30-32页
·协议状态转换	第32-34页
·协议的PROMELA模型	第34-48页
·建模假定	第35-36页
·模型结构	第36-37页
·TR-Service模型结构	第37-43页
·TR-Protocol模型结构	第43-47页
·仿真的运行	第47-48页
·协议的正确属性需求规范	第48-51页
·安全属性	第48-49页
·活性	第49-50页
·时序行为	第50-51页
·总结	第51-52页
第四章 基于SPIN的WTP协议验证	第52-58页
·验证结果	第53-58页
·对TR-Service模型的正确属性进行验证	第53-54页
·TR-Protocol协议中的错误	第54-58页
第五章 结论与展望	第58-59页
·论文的主要工作	第58页
·进一步的工作	第58-59页
致谢	第59-60页
参考文献	第60-62页
附录1 攻读硕士学位期间的主要工作	第62-63页