随着网络的普及和Web技术的迅速发展,人们迫切需要在Internet上实现跨平台、语言独立、松散耦合的异构应用的集成和交互,这对传统的分布式计算技术提出了新的要求。Web服务作为一种新型的分布式计算模型应运而生,成为网络上数据和信息集成的有效机制。服务组合是将现有的可用Web服务组合起来、协同执行,形成功能更强大的增值服务。为了满足不同Web服务之间运行结果的一致性和可靠性要求,我们需要在Web服务组合中提供事务处理的支持。Web服务事务不同于传统的ACID事务,不能通过简单回滚来恢复已完成的动作,因此,需要采用补偿机制来保证数据的一致性。按照不同的补偿安装方式,可将补偿模型分为静态和动态补偿模型。静态补偿模型的补偿不是随着事务的执行而动态安装的,因此这种方法缺乏灵活性,容易在复杂的网络环境中发生错误。而很多动态补偿模型是基于流的,即采用集中式的协调机制,缺乏移动性,不能有效地模拟结构不断变化的Web服务系统。尽管目前存在着多种补偿模型,但他们之间的关系并不是很清楚,而且表达能力的比较分析工作才刚刚起步。随着Web服务的发展,使用形式化方法研究Web服务已成为一个重要研究内容。其中以π-演算为代表的移动进程演算,比较适合研究交互服务的行为,因此可以很自然地应用于Web服务的建模和开发之中。本文的工作主要围绕Web服务事务及其补偿处理的形式化研究而展开的。本文的主要研究内容及成果如下：1.建立了一般动态的Web服务事务补偿模型通过{P；R}n、n、[P]及a(x)%[λX.Q].P对标准的π-演算进行扩展,定义Exπ演算作为Web服务事务的一般动态补偿模型,同时给出了相应的操作语义。该模型的输入动作可以激活补偿更新,因此补偿进程可以随着事务的交互而动态安装起来。为保证事务的唯一性,我们在该模型中增加了一个简单类型系统。通过该补偿演算对Web服务实例的形式化描述,充分展示了该模型的灵活性和表达能力。该模型独立于具体的Web服务语言和方案,可以使我们更好地理解和把握Web服务及其事务补偿的本质特征。2.比较不同补偿模型的表达能力用扩展的π-演算对静态、并行动态和一般动态补偿模型进行统一的形式化描述。简化Exπ演算使得任意动作都可以激活补偿更新,我们称其为Exπ′模型。递增地定义了这三类补偿模型的语法,同时给出了相应的操作语义。本文定义了演算的编码条件,提出了弱互模拟关系和should测试等价概念。我们将并行动态编码成静态补偿演算,证明了静态和并行动态补偿演算具有相同的表达能力。最后,本文证明了不能把一般动态编码成静态补偿演算,从而论证了Exπ′模型具有较强的表达能力。