| 摘要 | 第1-7页 |
| ABSTRACT | 第7-15页 |
| 1 绪论 | 第15-26页 |
| ·研究背景 | 第15-17页 |
| ·研究动机 | 第17-19页 |
| ·国内外研究现状 | 第19-22页 |
| ·论文主要工作 | 第22-24页 |
| ·论文组织结构 | 第24-26页 |
| 2 进程代数理论 | 第26-35页 |
| ·通信顺序进程CSP | 第27-30页 |
| ·事件和进程 | 第27-28页 |
| ·进程的递归表示 | 第28页 |
| ·进程的顺序执行 | 第28-29页 |
| ·进程的并发 | 第29-30页 |
| ·进程间的通信 | 第30页 |
| ·Pi-演算 | 第30-35页 |
| ·Pi-演算的语法定义 | 第30-32页 |
| ·Pi-演算的同构规则 | 第32页 |
| ·Pi-演算的操作语义 | 第32-35页 |
| 3 BPEL4WS 的形式化模型 | 第35-57页 |
| ·问题概述 | 第35页 |
| ·BPEL4WS Web 服务组合规范 | 第35-36页 |
| ·基于 Pi-演算的 BPEL4WS 形式化模型 | 第36-44页 |
| ·从BPEL4WS 到Pi-演算的概念映射 | 第36-37页 |
| ·BPEL4WS 原子行为 | 第37-40页 |
| ·BPEL4WS 结构化行为 | 第40-42页 |
| ·BPEL4WS 并发行为 | 第42页 |
| ·BPEL4WS 异常处理 | 第42-43页 |
| ·BPEL4WS 事件处理 | 第43页 |
| ·BPEL4WS 补偿处理 | 第43-44页 |
| ·基于CSP 的BPEL4WS 形式化模型 | 第44-46页 |
| ·BPEL4WS 到形式化模型的自动转换 | 第46-50页 |
| ·模型的验证 | 第50-56页 |
| ·与同类工作的比较 | 第56页 |
| ·本章小结 | 第56-57页 |
| 4 WS-CDL 的形式化模型框架 | 第57-85页 |
| ·问题概述 | 第57页 |
| ·WS-CDL Web 服务组合规范 | 第57-60页 |
| ·Abstract WS-CDL 形式化模型框架 | 第60-64页 |
| ·基本概念的形式化描述 | 第60-61页 |
| ·Abstract WS-CDL 的语法 | 第61-62页 |
| ·Abstract WS-CDL 的同构关系 | 第62-63页 |
| ·Abstract WS-CDL 的操作语义 | 第63-64页 |
| ·从 WS-CDL 到 Abstract WS-CDL 的转换 | 第64-70页 |
| ·WS-CDL 的原子行为 | 第65-68页 |
| ·WS-CDL 的结构化行为 | 第68-70页 |
| ·WS-CDL 的并发行为 | 第70页 |
| ·从 Choreography 到 Orchestration 的映射 | 第70-73页 |
| ·Choreography 和 Orchestration 的一致性 | 第73-75页 |
| ·模型验证 | 第75-83页 |
| ·与同类工作的比较 | 第83-84页 |
| ·本章小结 | 第84-85页 |
| 5 Web 服务组合的相容性和可替换性形式化描述 | 第85-101页 |
| ·问题概述 | 第85-86页 |
| ·二个 Web 服务的强互相容性 | 第86-89页 |
| ·二个 Web 服务的弱互相容性 | 第89-91页 |
| ·多个 Web 服务的互相容性 | 第91-93页 |
| ·Web 服务的可替换性 | 第93-94页 |
| ·Web 服务的相容性检测算法 | 第94-96页 |
| ·案例分析 | 第96-99页 |
| ·与同类工作的比较 | 第99-100页 |
| ·本章小结 | 第100-101页 |
| 6 类型化的BPEL4WS 形式化模型 | 第101-121页 |
| ·问题概述 | 第101页 |
| ·扩充的 Pi-演算类型系统 | 第101-113页 |
| ·基本定义 | 第102页 |
| ·基本语法 | 第102-104页 |
| ·类型判定规则 | 第104-110页 |
| ·进程操作语义 | 第110-113页 |
| ·类型化的BPEL4WS 形式化模型 | 第113-116页 |
| ·模型验证 | 第116-119页 |
| ·与同类工作的比较 | 第119-120页 |
| ·本章小结 | 第120-121页 |
| 7 类型化的WS-CDL 形式化模型框架 | 第121-145页 |
| ·问题概述 | 第121-122页 |
| ·Interaction 行为的数据类型一致性分析 | 第122-123页 |
| ·基本定义 | 第123-124页 |
| ·Typed Abstract WS-CDL 基本语法 | 第124-125页 |
| ·类型定义 | 第124页 |
| ·值定义 | 第124页 |
| ·会话定义 | 第124-125页 |
| ·类型假设集和子类型关系 | 第125页 |
| ·Typed Abstract WS-CDL 类型判定规则 | 第125-128页 |
| ·值类型判定规则 | 第125页 |
| ·子类型关系判定规则 | 第125-126页 |
| ·会话类型良好判定规则 | 第126-128页 |
| ·Typed Abstract WS-CDL 操作语义 | 第128-130页 |
| ·会话的类型假设集的构造与合并 | 第130-132页 |
| ·类型化的 Choreography 到 Orchestration 的映射 | 第132-136页 |
| ·Typed Abstract WS-CDL 的性质 | 第136-139页 |
| ·模型验证 | 第139-142页 |
| ·进一步讨论 | 第142-143页 |
| ·与同类工作的比较 | 第143-144页 |
| ·本章小结 | 第144-145页 |
| 8 面向应用的 Web 服务组合实现框架 | 第145-152页 |
| ·体系结构 | 第145-146页 |
| ·iFrame4WS 描述层 | 第146-149页 |
| ·iFrame4WS 抽象层 | 第149-151页 |
| ·iFrame4WS 执行层 | 第151页 |
| ·本章小结 | 第151-152页 |
| 9 总结与未来的工作 | 第152-155页 |
| ·论文总结 | 第152-153页 |
| ·论文的不足以及未来工作展望 | 第153-155页 |
| 致谢 | 第155-156页 |
| 参考文献 | 第156-167页 |
| 附录1 攻读学位期间发表的论文目录 | 第167-168页 |
| 附录2 攻读学位期间参加的科研项目 | 第168-169页 |
| 附录3 第3 章案例验证代码 | 第169-171页 |
| 附录4 第4 章案例验证代码 | 第171-176页 |
| 附录5 第6 章案例验证代码 | 第176页 |
