当今,Web服务是实现应用系统间互操作的最有前途的互联网技术。Web服务平台的基础是一系列依赖于XML技术的标准。其中,Web服务组合是实现商业系统集成的关键。除了服务交互、控制流协调之外,Web事务的支持对服务组合来说也是必不可少的,它能有效地保证合成服务的可靠执行以及系统状态的一致性。然而,现有的技术缺乏对Web事务的支持。与传统事务不同,Web事务具备长时间运行、强自治性、交互性的特点,因此经典的事务处理技术如资源锁定、自动回滚等都不适用于Web事务。本文采用形式化的方法来研究Web事务。首先,我们提出了一种新型的事务语言,简称为t演算。它采用补偿机制来处理事务中途出现的故障,并在一定程度上弱化了Web事务对原子性的需求。t演算的核心构造是可补偿事务,而Web事务被视为可补偿事务的有机组合。此事务语言不仅扩展了传统算子对补偿的支持,还引入了一些新的事务组合算子,例如:投机选择、候补恢复、异常处理以及编制补偿。这些新算子不但结合了后向恢复和前向恢复的机制,还大大提高了事务流程的可靠性和灵活性。此外,补偿流本身也可以是可补偿事务,这种安排使得设计人员能够以一种统一的方式对前向流和补偿流进行管理。接下来,我们对此事务语言展开了形式语义的分析,为事务流程和补偿机制提供了精确的刻画。我们建立了三种不同的语义模型,旨在帮助开发者从不同的视角对Web事务进行观察,从而能更好的理解事务处理机制。代数语义研究可补偿事务的代数性质,为事务流程的转换和优化奠定基础。在代数模型中,首先指定规范型,然后定义代数规则把任意的可补偿事务重写为规范型,通过符号计算的方式得到一系列描述事务性质的代数定律。操作语义通过变迁规则来研究事务的演化过程,它有助于事务流程的模拟与测试。操作模型中,针对事务的补偿性特点,我们定义了双模拟关系用来研究事务之间的等价性。指称语义在数学模型的基础上对事务的整体行为进行严格的解释。这里,我们扩展了“迹”的概念,引申出“对迹”这一新的模式来刻画可补偿事务的行为,并通过对迹行为来定义事务的等价关系。不同语义模型对同一物理概念可能给出不同的解释.为了避免二义性,我们采用UTP理论来研究各种语义模型间的一致性关系.本文中,各种语义模型并不是独立定义的.相反,我们先从代数语义出发,得到一系列描述事务性质的代数定律.然后通过定义推导规则,从代数语义推导出操作语义,类似的,再从操作语义推导出指称语义。接下来,我们证明了代数语义中的代数定律在操作语义和指称语义中也都是成立的。这样,不同语义模型间的一致性就得到了保证,而且也为语义模型自身的正确性提供了进一步的保障。最后,我们对事务语言进行了扩展,加入了数据操作和服务交互的信息。在实现Web事务的基础上,为服务的设计开发提供了进一步的支持。对于扩展后的语言,我们采用面向观察的语义对服务行为进行刻画,建立了多个行为侧面(包括数据状态、交互序列以及事务行为)在执行前后的演化关系。此外,我们还对可补偿事务的精化关系给出了形式化的定义,为服务的规范与实现搭建了桥梁。总之,采用形式化的方法对Web事务进行研究,一方面可以帮助设计者更好的理解Web事务的工作机制,消除可能存在的二义性;另一方面用来支持测试、验证工具的开发,为软件系统的质量提供有力的保障。