| 摘要 | 第1-7页 |
| ABSTRACT | 第7-9页 |
| 缩略语 | 第9-10页 |
| 目录 | 第10-16页 |
| 第一章 绪论 | 第16-36页 |
| ·课题研究背景 | 第16-19页 |
| ·开放分布式处理的发展--Web服务 | 第16-17页 |
| ·转向服务计算 | 第17-19页 |
| ·数理逻辑—系统建模与推理 | 第19页 |
| ·服务计算与Web服务协议栈 | 第19-31页 |
| ·如何理解Web服务 | 第20页 |
| ·Web服务的技术架构 | 第20-21页 |
| ·基础变化:XML—数据表示方式 | 第21-22页 |
| ·传送协议:SOAP及其性能 | 第22-24页 |
| ·WSDL:描述服务 | 第24-26页 |
| ·UDDI:发布/发现Web服务 | 第26-27页 |
| ·Web服务的上层设施 | 第27-31页 |
| ·服务计算国内外研究现状 | 第31-34页 |
| ·作者的主要工作 | 第34页 |
| ·本章小结及本文的章节安排 | 第34-36页 |
| 第二章 面向服务的计算SOC | 第36-55页 |
| ·服务计算的概念 | 第36-40页 |
| ·服务计算的体系结构 | 第40-43页 |
| ·服务计算的建模和开发语言 | 第43-49页 |
| ·OMG建模的四个层次 | 第43-46页 |
| ·更多的层次 | 第46-47页 |
| ·服务建模语言 | 第47-49页 |
| ·服务计算的开发环境 | 第49-51页 |
| ·XML Web服务和.NET框架 | 第49页 |
| ·BizTalk框架 | 第49-50页 |
| ·SUN Java Web服务 | 第50页 |
| ·IBM开发环境WSAD | 第50-51页 |
| ·其它环境 | 第51页 |
| ·服务计算的技术框架 | 第51-53页 |
| ·小结 | 第53-55页 |
| 第三章 SOC中的服务组合及其形式化方法 | 第55-73页 |
| ·服务组合的概念—工作流技术与服务组合 | 第55-57页 |
| ·工作流技术 | 第55-56页 |
| ·服务组合与工作流 | 第56-57页 |
| ·服务组合的需求 | 第57页 |
| ·服务组合的主要方法 | 第57-60页 |
| ·BPEL | 第58页 |
| ·语义Web(OWL-S) | 第58-59页 |
| ·代数化的服务组合 | 第59页 |
| ·Petri网 | 第59-60页 |
| ·模型检查和有限状态自动机FSM | 第60页 |
| ·半形式化方法UML | 第60页 |
| ·服务组合方法的比较 | 第60-62页 |
| ·连接性和非功能属性 | 第60-61页 |
| ·组合正确性 | 第61页 |
| ·自动组合 | 第61页 |
| ·组合伸缩性 | 第61-62页 |
| ·进程代数方法 | 第62-69页 |
| ·进程代数的定义 | 第62-64页 |
| ·描述并发语义 | 第64-65页 |
| ·经典进程代数方法 | 第65-67页 |
| ·进程代数的发展 | 第67-69页 |
| ·服务计算对进程代数的挑战 | 第69-71页 |
| ·松散耦合 | 第69-70页 |
| ·通信延迟 | 第70页 |
| ·开放式终端 | 第70-71页 |
| ·无中心的服务编排 | 第71页 |
| ·相关研究工作 | 第71-72页 |
| ·小结 | 第72-73页 |
| 第四章 服务组合的正确性验证 | 第73-86页 |
| ·服务组合中的形式化方法 | 第73页 |
| ·服务组合的正确性及其验证方法-基于Pi演算 | 第73-76页 |
| ·服务组合的正确性 | 第74页 |
| ·正确性的验证方法 | 第74页 |
| ·Pi演算 | 第74-76页 |
| ·Pi演算与Web服务元素的对应关系 | 第76-78页 |
| ·服务组合的正确性验证实例 | 第78-84页 |
| ·机票预定服务的描述 | 第78-81页 |
| ·描述服务的动态变化 | 第81-82页 |
| ·利用Pi演算对系统进行推演和验证 | 第82-84页 |
| ·相关研究工作 | 第84-85页 |
| ·小结 | 第85-86页 |
| 第五章 服务组合的一致性验证 | 第86-123页 |
| ·服务组合的一致性概念 | 第86-100页 |
| ·业务流程执行语言WS BPEL | 第86-93页 |
| ·BPEL4WS语言的基本结构 | 第87-88页 |
| ·最高级别的属性 | 第88页 |
| ·活动 | 第88-91页 |
| ·合作伙伴链接类型、合作伙伴链接和端点引用 | 第91-92页 |
| ·变量 | 第92页 |
| ·相关性 | 第92页 |
| ·补偿处理和故障处理 | 第92-93页 |
| ·Web服务编排描述语言WS CDL | 第93-99页 |
| ·WS CDL与WS BPEL的一致性 | 第99-100页 |
| ·支持SOA设计的服务编排形式化框架 | 第100-111页 |
| ·基于Pi演算的Web服务编排描述 | 第100-102页 |
| ·基于Pi演算的WS CDL形式化验证框架 | 第102-111页 |
| ·框架建立原则 | 第102-103页 |
| ·推理规则和验证方法 | 第103-106页 |
| ·异步消息交换 | 第106页 |
| ·基于形式化框架建模和验证一个具体的服务编排 | 第106-111页 |
| ·模型驱动的服务组合设计 | 第111-113页 |
| ·服务组合的一致性验证 | 第113-119页 |
| ·Pi演算模型到WS CDL的转换规则 | 第113-115页 |
| ·WS CDL到WS BPEL的转换规则 | 第115-116页 |
| ·实例说明 | 第116-119页 |
| ·相关研究工作 | 第119-121页 |
| ·小结 | 第121-123页 |
| 第六章 服务组合的可替换性验证 | 第123-136页 |
| ·服务组合的兼容性概念 | 第123页 |
| ·使用Pi演算作为形式化基础 | 第123-124页 |
| ·服务组合的可替换性验证 | 第124-127页 |
| ·Web服务可替换的充分条件 | 第124页 |
| ·用Pi演算描述Web服务兼容性 | 第124-125页 |
| ·弱互模拟满足可替换性条件的证明 | 第125-126页 |
| ·异步Web服务可替换性 | 第126-127页 |
| ·服务组合的可替换性实例 | 第127-133页 |
| ·相关研究工作 | 第133-134页 |
| ·小结 | 第134-136页 |
| 第七章 服务组合框架PIFF | 第136-152页 |
| ·模型驱动的服务组合(MDSC) | 第136-138页 |
| ·模型驱动体系结构(MDA)与面向服务体系结构(SOA) | 第136-138页 |
| ·服务组合中的模型方法 | 第138页 |
| ·基于Pi演算的模型驱动服务组合设计框架PiFF | 第138-147页 |
| ·UESTC-PLATFORM:一个服务计算可视化平台 | 第139-141页 |
| ·基于Pi演算的形式化框架PiFF | 第141-147页 |
| ·PiFF:一个基于Pi演算的形式化框架 | 第141-142页 |
| ·WS CDL,WS BPEL和pi演算元素的对应关系 | 第142-143页 |
| ·将高级结构映射到Pi演算 | 第143-144页 |
| ·PiFF框架的验证方法 | 第144-146页 |
| ·PiFF框架的验证工具 | 第146-147页 |
| ·使用PiFF框架的实例 | 第147-149页 |
| ·PiFF与UESTC-PLATFORM的融合研究 | 第149-150页 |
| ·相关研究工作 | 第150-151页 |
| ·小结 | 第151-152页 |
| 第八章 全文总结及进一步的工作 | 第152-155页 |
| ·全文总结 | 第152-153页 |
| ·进一步的工作 | 第153-155页 |
| 参考文献 | 第155-169页 |
| 致谢 | 第169-170页 |
| 攻博期间取得的研究成果 | 第170-171页 |
| 一.个人简历 | 第170页 |
| 二.科研成果 | 第170页 |
| 三.论文发表 | 第170-171页 |
| 四.获奖情况 | 第171页 |
