| 摘要 | 第1-4页 |
| Abstract | 第4-6页 |
| 目录 | 第6-10页 |
| 第一章 绪论 | 第10-19页 |
| ·研究背景 | 第10-11页 |
| ·研究现状和发展 | 第11-12页 |
| ·本课题的主要工作 | 第12-18页 |
| ·研究设想和主要研究内容 | 第12-14页 |
| ·研究的依据 | 第14-16页 |
| ·研究难点和解决方案 | 第16-17页 |
| ·本文的主要贡献和创新之处 | 第17-18页 |
| ·论文的组织 | 第18-19页 |
| 第二章 BPEL4WS规范和pi演算理论 | 第19-25页 |
| ·BPEL4WS语言 | 第19-20页 |
| ·pi演算 | 第20-23页 |
| ·pi演算的基本语法 | 第21-22页 |
| ·pi演算的迁移语义 | 第22-23页 |
| ·扩充pi演算的语法和语义 | 第23-25页 |
| 第三章 BPEL4WS程序的形式化建模 | 第25-47页 |
| ·DPE机制的研究 | 第25-28页 |
| ·BPEL4WS规范中DPE机制的定义 | 第25-26页 |
| ·DPE机制带来的效应 | 第26页 |
| ·DPE效应的处理 | 第26-28页 |
| ·link的pi演算表示 | 第28-29页 |
| ·joinCondition的pi演算表示 | 第29-30页 |
| ·BPEL4WS活动的形式化描述 | 第30-38页 |
| ·外部原子活动的建模 | 第30-33页 |
| ·结构化活动的建模 | 第33-38页 |
| ·出错和补偿机制的建模 | 第38-42页 |
| ·关于scope的建模 | 第42-43页 |
| ·建模实例 | 第43-46页 |
| ·本章小结 | 第46-47页 |
| 第四章 Pi演算上的类型系统研究 | 第47-63页 |
| ·多元pi演算的规约语义 | 第47-50页 |
| ·规约语义定义 | 第47-48页 |
| ·结构同余 | 第48-49页 |
| ·运行时错误 | 第49-50页 |
| ·pi演算上的类型系统 | 第50-52页 |
| ·类型定义 | 第50-51页 |
| ·递归类型 | 第51-52页 |
| ·类型互模拟 | 第52-56页 |
| ·观察 | 第52页 |
| ·类型互模拟关系 | 第52-53页 |
| ·类型互模拟性质 | 第53-56页 |
| ·上下文环境 | 第56-57页 |
| ·子类型关系 | 第57-59页 |
| ·进程类型定义良好规则 | 第59-61页 |
| ·类型化pi演算规约语义 | 第61-62页 |
| ·本章小结 | 第62-63页 |
| 第五章 Web服务组合的相容性分析 | 第63-82页 |
| ·相容性定义 | 第64-65页 |
| ·基于类型化pi演算的Web服务组合相容性分析算法 | 第65-66页 |
| ·BPEL4WS和服务的类型化pi演算建模 | 第66-72页 |
| ·BPEL4WS的类型化pi演算建模 | 第66-69页 |
| ·服务的类型化pi演算建模 | 第69-72页 |
| ·Web服务组合的相容性分析实例 | 第72-79页 |
| ·反例研究 | 第79-80页 |
| ·本章小结 | 第80-82页 |
| 第六章 scope的ambient演算建模的尝试 | 第82-90页 |
| ·ambient演算简介 | 第82-85页 |
| ·ambient演算的语法 | 第82-84页 |
| ·ambient演算的操作语义 | 第84-85页 |
| ·异步pi演算的编码 | 第85-86页 |
| ·ambiet演算编码SCOPE | 第86-89页 |
| ·小结 | 第89-90页 |
| 第七章 总结与展望 | 第90-92页 |
| 参考文献 | 第92-98页 |
| 附录1 BPEL4WS建模规则 | 第98-101页 |
| 附录2 旅游预订例子BEPL4WS程序 | 第101-104页 |
| 附录3 贷款审批.bpel | 第104-108页 |
| 附录4 贷款审批.wsdl | 第108-114页 |
| 附录5 信用度查询.wsdl | 第114-116页 |
| 附录6 数据入库服务.wsdl | 第116-117页 |
| 附录7 短信发送服务.wsdl | 第117-118页 |
| 附录8 攻读硕士期间发表的学术论文 | 第118-120页 |
| 附录9 致谢 | 第120-122页 |
| 附录10 湖南师范大学学位论文原创性声明 | 第122页 |