| 作者简介 | 第1-4页 |
| 摘要 | 第4-6页 |
| ABSTRACT | 第6-11页 |
| 第一章 绪论 | 第11-19页 |
| ·研究背景和意义 | 第11-12页 |
| ·研究现状 | 第12-16页 |
| ·研究内容和章节安排 | 第16-19页 |
| 第二章 Web 服务组合与 BPEL | 第19-25页 |
| ·BPEL 的活动介绍 | 第19-22页 |
| ·基本活动 | 第19-21页 |
| ·结构化活动 | 第21-22页 |
| ·BPEL 活动中的 Flow（流程）分析 | 第22-24页 |
| ·Flow 相关的标准属性和元素 | 第22-23页 |
| ·Link 的语义 | 第23页 |
| ·Flow 中的活动启动 | 第23-24页 |
| ·BPEL 控制流中的死路径删除 | 第24页 |
| ·小结 | 第24-25页 |
| 第三章 有色 Petri 网及 BPEL 活动建模 | 第25-47页 |
| ·Petri 网介绍 | 第25-27页 |
| ·Petri 的形式化定义 | 第25-26页 |
| ·Petri 的运行规则 | 第26页 |
| ·高级 Petri | 第26-27页 |
| ·有色 Petri 网 | 第27-30页 |
| ·CP-nets 的形式化定义 | 第27-30页 |
| ·CP-nets 的作用和工具 | 第30页 |
| ·赋时 CP-nets 网 | 第30-31页 |
| ·BPEL 活动模型 | 第31-45页 |
| ·模型中用到的变量声明 | 第31-32页 |
| ·基本活动（Basic Activities） | 第32-34页 |
| ·结构化活动（Struct Activities） | 第34-38页 |
| ·Flow Activity （流活动） | 第38-45页 |
| ·模型分析 | 第45页 |
| ·小结 | 第45-47页 |
| 第四章 层次化构建 BPEL 模型 | 第47-61页 |
| ·层次化 CP-nets 的形式化定义 | 第47-49页 |
| ·层次化 CP-nets 的等价非层次化 CP-nets | 第49-50页 |
| ·BPEL 服务组合的层次化 CP-nets 建模 | 第50-56页 |
| ·BPEL 的错误处理机制 | 第51-52页 |
| ·具有错误处理机制的 BPEL 层次模型 | 第52-55页 |
| ·BPEL 服务组合的层次化建模方法 | 第55-56页 |
| ·BPEL 服务组合建模方法的应用 | 第56-59页 |
| ·小结 | 第59-61页 |
| 第五章 Web 服务组合流程的 CP-nets 模型验证 | 第61-69页 |
| ·模型验证的基本思想 | 第61-62页 |
| ·Kripke 结构（Kripke Structure） | 第61-62页 |
| ·模型验证的基本思想 | 第62页 |
| ·模型验证包含的活动 | 第62页 |
| ·扩展时态逻辑 ASK-CTL | 第62-65页 |
| ·服务组合流程的模型验证 | 第65-67页 |
| ·CP-nets 的一般属性 vs 服务组合流程的性质 | 第65-66页 |
| ·使用 ASK-CTL 表示 CP-nets 的动态属性 | 第66-67页 |
| ·小结 | 第67-69页 |
| 第六章 基于抽象的 CP-nets 模型安全属性验证 | 第69-97页 |
| ·反例引导的抽象-细化 | 第69-70页 |
| ·谓词抽象 | 第70-74页 |
| ·谓词抽象的相关概念 | 第70-74页 |
| ·谓词细化 | 第74页 |
| ·CP-nets 模型的谓词抽象算法 | 第74-80页 |
| ·谓词抽象算法 | 第74-76页 |
| ·谓词抽象算法应用实例 | 第76-80页 |
| ·惰性抽象 | 第80-86页 |
| ·惰性抽象的相关概念 | 第82-84页 |
| ·惰性抽象算法 | 第84-86页 |
| ·CP-nets 模型的惰性抽象算法 | 第86-95页 |
| ·CP-nets 模型与惰性抽象的先决条件 | 第86-87页 |
| ·CP-nets 模型可达树的结点分类 | 第87-88页 |
| ·CP-nets 模型的惰性抽象算法 | 第88-91页 |
| ·惰性抽象算法应用实例 | 第91-95页 |
| ·小结 | 第95-97页 |
| 第七章 Web 服务组合测试用例生成技术研究 | 第97-115页 |
| ·研究背景 | 第97页 |
| ·测试覆盖标准 | 第97-100页 |
| ·现有的 BPEL 测试度量标准 | 第98-100页 |
| ·基于 CP-nets 模型的 BPEL 并发路径测试度量标准 | 第100页 |
| ·BPEL 单元测试方法 | 第100-110页 |
| ·基于 CP-nets 的 BPEL 模型分析 | 第101-103页 |
| ·基于控制流的程序可执行单元生成算法 | 第103-104页 |
| ·约束处理算法 | 第104-107页 |
| ·无效可执行程序单元的剔除 | 第107-108页 |
| ·可并发执行的程序单元的变量共享问题 | 第108-110页 |
| ·测试用例生成 | 第110页 |
| ·实例研究 | 第110-112页 |
| ·小结 | 第112-115页 |
| 第八章 总结和展望 | 第115-117页 |
| ·本文工作总结 | 第115-116页 |
| ·未来工作展望 | 第116-117页 |
| 致谢 | 第117-119页 |
| 参考文献 | 第119-131页 |
| 攻读博士学位期间的研究成果 | 第131-133页 |
| 学术论文 | 第131-132页 |
| 参加研究的科研项目 | 第132-133页 |
