| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第一章 绪论 | 第8-16页 |
| ·研究背景及意义 | 第8-9页 |
| ·国内外研究现状 | 第9-13页 |
| ·Web服务的模型检测 | 第9-11页 |
| ·特征交互的模型检测 | 第11-13页 |
| ·安全协议的模型检测 | 第13页 |
| ·研究内容 | 第13-14页 |
| ·结构安排 | 第14-16页 |
| 第二章 模型检测技术 | 第16-29页 |
| ·时态逻辑 | 第16-18页 |
| ·计算树逻辑CTL* | 第16-17页 |
| ·分支时态逻辑CTL | 第17-18页 |
| ·线性时态逻辑LTL | 第18页 |
| ·符号化模型检测 | 第18-20页 |
| ·模型检测的原理 | 第18-19页 |
| ·符号化模型检测 | 第19-20页 |
| ·知识推理 | 第20-24页 |
| ·模型检测时态认知逻辑 | 第24-28页 |
| ·时态认知逻辑CKLn | 第24-25页 |
| ·符号化模型检测CKLn | 第25-27页 |
| ·时态认知逻辑的模型检测工具MCTK | 第27-28页 |
| ·小结 | 第28-29页 |
| 第三章 基于时态认知逻辑的Web服务模型检测 | 第29-48页 |
| ·Web服务及其形式化验证 | 第29-34页 |
| ·贷款批准协议Loan Approval protocol | 第34-39页 |
| ·系统建模 | 第34-35页 |
| ·系统智能体描述 | 第35-38页 |
| ·实验结果 | 第38-39页 |
| ·股票分析服务SAS协议 | 第39-44页 |
| ·系统建模 | 第40-41页 |
| ·系统智能体描述 | 第41-43页 |
| ·实验结果 | 第43-44页 |
| ·家具购买服务P& S协议 | 第44-47页 |
| ·系统建模 | 第44-45页 |
| ·系统智能体描述 | 第45-46页 |
| ·实验结果 | 第46-47页 |
| ·小结 | 第47-48页 |
| 第四章 基于时态认知逻辑的Web服务特征交互模型检测 | 第48-56页 |
| ·Web服务特征交互问题 | 第48-49页 |
| ·Web服务特征交互的模型检测 | 第49-50页 |
| ·系统建模 | 第50-51页 |
| ·系统智能体描述 | 第51-53页 |
| ·实验结果 | 第53-55页 |
| ·小结 | 第55-56页 |
| 第五章 Web服务的形式化验证框架体系 | 第56-64页 |
| ·Web服务形式化验证的框架 | 第56页 |
| ·Web服务形式化验证的转换过程 | 第56-61页 |
| ·从BPEL到一阶逻辑公式 | 第56-59页 |
| ·从一阶逻辑公式到类smv | 第59-61页 |
| ·实例说明 | 第61-63页 |
| ·实验结果 | 第63页 |
| ·小结 | 第63-64页 |
| 第六章 基于时态认知逻辑的安全协议的模型检测 | 第64-68页 |
| ·Needham-Schroeder安全协议 | 第64页 |
| ·系统建模 | 第64-66页 |
| ·系统智能体描述 | 第66-67页 |
| ·实验结果 | 第67页 |
| ·小结 | 第67-68页 |
| 第七章 结束与展望 | 第68-69页 |
| 参考文献 | 第69-74页 |
| 致谢 | 第74-75页 |
| 作者在攻读硕士期间主要研究成果 | 第75页 |