Web服务事务处理必须保证多个Web服务运行结果的可靠性和一致性，并能及时解决运行时发生的各种异常。目前已有的Web服务事务协议均不能提供确切的事务处理语义定义，严重阻碍了事务的实现，例如由IBM和Microsoft制定的WS-Coordination、WS-AT和WS-BA协议，以及由OASIS组织制定的BTP。这些规范放松了传统事务中的ACID属性的限制，重新定义了松耦合环境下的事务性质。但是，这些规范中存在一些问题，比如描述的不详细，有歧义等。因此在规范的实施中，迫切需要对这些事务协议进行形式化分析及验证，进一步完善这些规范，保证协议的正确实施。基于多元π演算，本文对Web服务事务协议：WS-AT和WS-BA进行了深入的研究，并提出了一个事务工作流的实现框架。本文的主要内容如下：首先，详细分析了事务的分类，按时间顺序可分为传统事务、移动事务和Web服务事务等；总结了事务的形式化研究现状，根据采用的语言可以分为三大方法：基于Petri网的形式化方法、基于进程代数的形式化方法和基于时序逻辑的形式化方法，并总结了每一种方法的优缺点；对Web服务事务实现的研究现状也作了深入地调查。其次，由于WS-AT采用简单的状态转换图和状态转换表，无法描述协调者和多个参与者的复杂协调活动，因此为规范协调行为，我们用π演算给出了WS-AT的形式化描述，并采用MWB工具的弱互模拟检验命令证明了WS-AT满足原子性。然后，由于WS-BA也是采用简单的状态转换图和状态转换表，并且没有给出内部状态的转变，导致当有多个参与者时，协调者不知如何协调它们的输出结果，为此我们提出了WS-BA中参与者主动提交协议的扩展：BAPC。用多元π演算建立了BAPC协议的形式化模型，并证明了BAPC协议满足长事务协议所具有的持久性、可终止性和局部原子性。最后，本文并没有局限于对WS-AT和WS-BA的形式化分析，根据这两个协议，在已有Web服务组合工作流引擎WebJetFlow上提出了事务工作流实现框架：TxWebJetFlow。通过扩展业务流程可执行语言BPEL和WebJetFlow的原有数据结构，加入原子事务和长事务协调机制，保证了组合Web服务的事务性质。综上所述，本文通过形式化方法来完善Web服务事务协议，提出了一个事务工作流的实现架框。对于发展我们的Web服务组合开发及运行平台具有重要的理论意义和实用价值。