| 摘要 | 第1-5页 |
| ABSTRACT | 第5-9页 |
| 第一章 绪论 | 第9-14页 |
| ·选题背景 | 第9-12页 |
| ·Web服务的发展 | 第9-10页 |
| ·形式化方法及其在Web服务中的研究应用 | 第10-11页 |
| ·形式化工具—π演算的优越性 | 第11-12页 |
| ·本文主要研究内容 | 第12-13页 |
| ·本文结构 | 第13-14页 |
| 第二章 Web服务技术及π演算概述 | 第14-23页 |
| ·Web服务的概念及特点 | 第14-15页 |
| ·Web服务的概念 | 第14页 |
| ·Web服务的体系结构 | 第14-15页 |
| ·Web服务的特征 | 第15页 |
| ·Web服务的相关技术和标准 | 第15-17页 |
| ·XML | 第15-16页 |
| ·SOAP | 第16-17页 |
| ·WSDL | 第17页 |
| ·UDDI | 第17页 |
| ·Orchestration)及Choreography技术 | 第17-20页 |
| ·Orchestration和Choreography的定义 | 第18-19页 |
| ·Orchestration与Choreography的关系 | 第19-20页 |
| ·π演算简述 | 第20-22页 |
| ·基本语法 | 第20-21页 |
| ·基本操作语义及进程上的结构同余 | 第21-22页 |
| ·小结 | 第22-23页 |
| 第三章 Web服务的事务处理 | 第23-28页 |
| ·经典事务的属性 | 第23页 |
| ·Web服务事务的特点 | 第23-24页 |
| ·Web服务事务处理机制 | 第24-27页 |
| ·OASIS BTP | 第24-25页 |
| ·WS-C/T | 第25-26页 |
| ·WS-CAF及WS-TXM | 第26-27页 |
| ·小结 | 第27-28页 |
| 第四章 基于π演算的Web服务组合模型 | 第28-35页 |
| ·引言 | 第28页 |
| ·模型的语法 | 第28-29页 |
| ·模型的语义 | 第29-32页 |
| ·模型描述的应用 | 第32-34页 |
| ·小结 | 第34-35页 |
| 第五章 Web服务事务的时间互模拟 | 第35-47页 |
| ·引言 | 第35页 |
| ·扩展实时π演算的语法、语义 | 第35-41页 |
| ·时间互模拟关系 | 第41-44页 |
| ·强时间互模拟关系 | 第41-43页 |
| ·弱时间互模拟关系 | 第43-44页 |
| ·基于时间粒的互模拟关系 | 第44-46页 |
| ·小结 | 第46-47页 |
| 第六章 结束语 | 第47-49页 |
| ·本文工作的总结 | 第47页 |
| ·进一步工作的讨论 | 第47-49页 |
| 参考文献 | 第49-52页 |
| 附录一 符号说明 | 第52-54页 |
| 致谢 | 第54-55页 |
| 攻读硕士学位期间发表和录用的文章 | 第55-56页 |
