基于进程代数的Web服务数据和组合的形式化方法研究

摘要

随着计算机网络的发展，Web服务日益成为分布式和异构应用的主流技术，它是一个崭新的分布式计算模型，是Web上数据和信息集成的有效机制。目前，Web服务已经成为计算机领域的一个研究热点。人们清楚地认识到Web服务的优势，越来越多的软件企业和研究机构纷纷加入到Web服务的开发和研究中。形式化方法已被用于基于消息通讯的并发系统的建模和分析。将形式化方法应用于Web服务领域已成为一个重要的研究方向。
　　在Web服务的各类研究中，Web数据与服务组合是其中的重要内容。基于进程代数的形式化方法研究了Web数据与服务组合的建模和验证。研究结果表明，形式化模型能保障Web数据的正确性与验证服务组合的性质。
　　Xdπ是一个具有代表性的Web数据模型，它能较好地反映分布式网络中数据与进程之间的交互。本文基于Xdπ建立起具有类型系统的Web数据形式化模型，定义了模型中各类数据的类型、类型判定式和类型规则集，并证明了该模型具有归约一致性。
　　业务流程执行语言（BPEL4WS）是基于编制的Web服务组合的语言标准，已被广泛用于业务流程的实现。实际应用对BPEL4WS程序提出了很高的要求。本文给出了对BPEL4WS建立基于传值CCS形式化模型的方法和具体实现算法，并对一个实例进行建模还验证无死锁的性质。
　　本文最后讨论了这一领域中的若干进一步研究问题。

目录

封面

目录

中文摘要

英文摘要

第一章 绪论

1.1 研究背景及意义

1.2 论文主要研究内容

1.3 论文结构

第二章 Web 服务

2.1 Web 服务的定义与特征

2.2 Web 数据

2.3 Web 服务组合

2.4 本章小结

第三章 进程代数

3.1 进程代数概述

3.2 通信系统演算 CCS

3.3 π -演算

3.4 本章小结

第四章 Web 数据的类型化模型

4.1 Web 数据的抽象

4.2 无类型的 Web 数据模型

4.3 类型系统

4.4 本章小结

第五章 基于传值 CCS 的 BPEL4WS 的形式化描述

5.1 BPEL4WS 和传值 CCS

5.2 BPEL4WS 基本活动的建模

5.3 BPEL4WS 到传值 CCS 的自动映射方法

5.4 一个例子

5.5 本章小结

第六章 总结和进一步的工作

6.1 总结

6.2 进一步的工作

致谢

参考文献

攻读博士学位期间发表的学术论文和科研项目

声明