面向服务的计算(Service-Oriented Computing, SOC)是一种以Web服务作为基本组件的分布式计算模式，它支持开放、动态和异构环境下分布式应用的系统集成。Web服务正从最初关注描述、发布和交互向支持健壮的业务协作新阶段发展。为了保证面向服务的应用获得正确、一致的执行结果，大多数工作流和B2B协作应用程序都需要支持复杂的、长时间运行的业务事务。面向服务的业务流程除了关注服务组合业务流程的功能特性外，应该整合考虑合成之上的事务特性。如何设计正确的Web服务组合业务流程，让它们协同工作并保持一致，即确保面向服务的业务事务(Business Transactions for Services, BTS)正确地执行是当前一个具有挑战性的重要问题。本文从操作系统进程管理的视角提出了面向服务的业务事务的概念视图,将现阶段的事务处理归结为在业务流程执行过程中对服务、活动及流程的分层管理。从建模语言到验证方法、从建模分析到验证实现，本文为面向服务的业务事务的正确性保障建立了一套系统的解决方案。主要研究成果如下：(1)提出了一种支持非功能性描述的移动进程代数MPi-演算。根据应用语义需求引入进程作用域的概念，扩展了Pi-演算进程移动性的含义。用链接相对进程作用域的移动来表示进程的移动，使得MPi-演算能够描述组件之间交互行为的非功能属性，具有兼顾系统功能性和非功能性描述的表达能力。提出了一种膜互模拟关系，使得在进程作用域内部具有不同行为的两个进程也可以被认为是等价的，并引入了膜等价概念，得出与强/弱互模拟等价类似的性质。(2)提出了一种等价自动机转换的模型验证方法。MPi-演算能够被解释成标号迁移系统(Labelled Transition System, LTS)，NuSMV是基于Kripke结构(Kripke Structure, KS)的符号模型检验器，LTS与KS都属于状态自动机(StateAutomata)。根据元模型LTS和KS之间的语义映射关系，给出了从MPi-演算模型到NuSMV的输入语言SMV的语法转换规则。基于元模型定义的语义映射关系和语法转换规则可以提高模型转换的可复用性和可移植性。(3)在服务层研究了如何保持业务流程参与者之间的协调一致性问题，提出了支持业务事务验证的服务协调模型。针对Web服务事务标准(WS-TX)定义的参与者之间交互消息缺乏严格的语义，用Pi-演算形式化描述了WS-TX规范中定义业务活动事务的WS-BA协议，在此基础上建立了适用于多个参与者的服务协调模型，并验证分析了协议的安全性和活性。实验结果表明，基于服务协调模型的业务事务验证方法，能够有效地提高业务流程执行的可靠性和一致性。(4)在活动层研究了如何利用Web服务事务模型分析事务的等价性问题，提出了面向服务的柔性事务建模与分析方法。用MPi-演算对柔性事务模型进行了形式化描述，考虑进程行为的事务依赖性，提出了一种事务膜等价关系。通过一个典型的柔性事务实例，阐述了利用事务膜开互模拟分析事务等价关系的方法。实验结果表明，事务膜开互模拟分析方法能够判别事务等价关系，约简目标系统模型，有效降低系统验证的复杂度。(5)在流程层研究了如何保证跨组织业务流程的可靠性问题，提出了跨组织多业务事务的建模与验证方法。将进程的动作交互与跨组织膜活动建立动态关联，提出了跨组织多业务事务建模方法。验证分析了多业务事务中排他性、响应性、非阻塞性和非平凡性等关键性质。实验结果表明，对于复杂的多业务事务，经过抽象或分解后，同样能够采用该方法保障多业务流程在设计与实现过程中的可靠性。(6)提出了基于策略的面向服务的业务事务验证支撑系统框架，提供了一种事务运行时的验证机制。设计和实现了面向服务的业务事务形式化验证原型工具VBT4S(Verification ofBusiness Transactions for Services)，支持主流开源的符号模型检验器NuSMV2。实验结果表明，系统支持非功能属性(如事务的完整性和一致性等)相关命题性质的模型检测，具有功能和非功能性质的统一验证与分析能力。