Web服务是解决分布式结构异构性的计算模型,Web服务中的事务处理是保证服务结果一致性和可靠性的有效技术。由于Web服务自身的分布性、异构性、自描述等特点,Web服务中的事务处理也具有长周期、自治性等特点,传统的事务处理技术不再适应。为解决些问题,工业界提出新的事务处理协议,如BTP、WS-C/Tx、WS-CAF、THP等协议。学术上,形式化方法已被用于对基于消息通讯的并发系统的建模和分析,模型检测方法在协议分析上有着抽象、高效等特点。因此将形式化方法用于Web服务领域已经成为一个重要的研究方向。本文采用形式化方法对支持事务协调的THP协议进行建模与验证分析。从“结构组件活性验证”与“业务逻辑安全性验证”两部分对THP协议进行建模和分析。针对THP协议的并发特性,采用Pi-演算进行建模,给出THP协议结构组件到Pi演算语法的映射表和建模规则。在对THP协议各个模块建模的基础上,得到THP协议结构组件的Pi-演算模型,然后运用Pi-演算模型检测工具MWB对THP协议结构组件的死锁性进行检测,从而验证了在并发情况下,THP协议各结构组件不会产生死锁。另一方面,对THP协议的业务逻辑进一步验证。本文给出Schema中消息到Pi-演算的映射规则,以及THP协议中WSDL描述到Pi-演算的编码规则,从元模型层实现了THP协议规范到Pi-演算的映射方法,为THP协议业务逻辑实例的Pi-演算建模提供了分析的基础。由于MWB不支持时间算子和相关的逻辑性质规约的推演,本文采用支持LTL的SAL,对模型的性质进行刻画、检测,通过反例的生成解释了通信中为什么存在不同步的现象。最后给出THP协议的应用实例,并对其建模以检测是否满足期望的性质,针对出现的问题给出解决方案,实现了模型检测方法对Web服务业务流程的管理与设计的指导作用。