| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第一章 绪论 | 第8-15页 |
| ·研究背景及意义 | 第8-9页 |
| ·国内外研究现状 | 第9-13页 |
| ·研究内容 | 第13-14页 |
| ·文章结构 | 第14-15页 |
| 第二章 组合Web 服务的特征交互问题及其模型检测 | 第15-20页 |
| ·Web 服务组合定义 | 第16页 |
| ·Web 服务组合特征交互问题简述 | 第16-17页 |
| ·Web 服务组合特征交互问题验证 | 第17-19页 |
| ·本章小结 | 第19-20页 |
| 第三章 模型检测技术 | 第20-31页 |
| ·时态逻辑 | 第20-23页 |
| ·线性时态逻辑LTL | 第21-22页 |
| ·计算树逻辑CTL* | 第22-23页 |
| ·分支时态逻辑CTL | 第23页 |
| ·符号化模型检测 | 第23-25页 |
| ·模型检测原理 | 第23-24页 |
| ·符号化模型检测 | 第24-25页 |
| ·知识推理 | 第25-28页 |
| ·关于可能世界模型 | 第25-27页 |
| ·知识的性质 | 第27-28页 |
| ·时态认知逻辑的模型检测 | 第28-30页 |
| ·时态知识逻辑CKLn | 第28-29页 |
| ·基于时态认知逻辑的模型检测工具MCTK | 第29-30页 |
| ·本章小结 | 第30-31页 |
| 第四章 Web 服务业务流程及其特征交互问题自动化模型检测 | 第31-68页 |
| ·Web 服务业务流程描述语言WS-BPEL | 第31-40页 |
| ·WS-BPEL 概念及相关规范 | 第31-33页 |
| ·WS-BPEL 组成 | 第33-35页 |
| ·WS-BPEL 活动语义分析 | 第35-39页 |
| ·选择BPEL4WS 的原因 | 第39-40页 |
| ·BPEL 流程的形式化模型及活动执行语义 | 第40-54页 |
| ·有限状态自动机 | 第40-41页 |
| ·智能体执行的形式化模型 | 第41-44页 |
| ·BPEL 活动执行语义以及相关七元组的产生 | 第44-54页 |
| ·BPEL 语言的自动化模型检测方法 | 第54-67页 |
| ·将BPEL 模型转化为迁移七元组 | 第54-61页 |
| ·MCTK 的输入语言与智能体声明 | 第61-64页 |
| ·将七元组转化为MCTK 的输入语言 | 第64-67页 |
| ·本章小结 | 第67-68页 |
| 第五章 自动转换算法的应用 | 第68-91页 |
| ·VTA 及其形式化验证 | 第68-77页 |
| ·将流程转化为迁移七元组 | 第69-73页 |
| ·将迁移七元组转化为MCTK 输入代码 | 第73-75页 |
| ·验证规范 | 第75-77页 |
| ·STS 及其特征交互检测 | 第77-87页 |
| ·将流程转化为迁移七元组 | 第78-82页 |
| ·将迁移七元组转化为MCTK 输入代码 | 第82-85页 |
| ·验证规范 | 第85-87页 |
| ·F2T 算法应用 | 第87-90页 |
| ·本章小结 | 第90-91页 |
| 第六章 总结与展望 | 第91-93页 |
| 参考文献 | 第93-97页 |
| 致谢 | 第97-98页 |
| 作者在攻读硕士期间主要研究成果 | 第98页 |