原子Web服务实现Internet上的独立的无状态的业务逻辑，允许其他应用程序通过Internet连接对其进行调用。Web服务组合可把多个无状态的原子Web服务组装为有状态的复杂应用，可用于表达业务流程，已经日渐成为重要的应用与研究领域。形式化方法已被用于对基于消息通讯的并发系统的建模和分析。将形式化方法应用于Web服务领域已成为一个重要的研究方向。 本文用形式化方法研究了Web服务组合的建模和分析问题，特别研究了服务组合中异常处理和事务处理的建模、服务组合的权限控制，讨论了基于全局观点和局部观点的服务组合模型。有关研究成果说明，形式化模型在构建正确无误的服务组合系统方面可能发挥重要的作用。 业务流程执行语言(BPEL)是基于编制的Web服务组合的语言标准，已被广泛用于业务流程的实现。实际应用对BPEL程序的正确性提出了很高要求。为更好地理解BPEL语言，并支持对BPEL程序和规范的形式化验证，本文设计了一个进程代数小语言作为BPEL的形式化模型，给出了它的操作语义，并基于模型检查技术研究了服务正确性检验和与时间相关的检验问题。 为更好地支持长事务处理，BPEL提供了特殊的异常处理和补偿机制，这些机制的语义比较复杂，其中一些问题在BPEL语言规范里也没有定义清楚。本文研究了BPEL的异常和补偿机制导致的控制流，提出了补偿闭包和补偿上下文等概念，构造了相应的形式化模型，完整、清晰地刻画了这些机制的语义，证明了所定义模型的一些性质，并分析了BPEL语言的异常和补偿模型中存在的一些问题。 在实际业务流程应用中，组合的Web服务中的某些工作常常最终需要由“人”来完成，这个问题对组合模型产生了很大影响。本文基于时态逻辑定义了相关的访问控制概念，研究BPEL与访问控制模型的集成，给出了BPEL活动在访问控制框架下的语义，并讨论流程在访问控制约束下的可满足性问题和资源分派问题，提出一套基于模型检查的求解方法。针对业界新近提出的BPEL4People标准，建立了BPEL4People的CSP形式化模型。 为开发正确的基于多个参与方的Web服务组合，近年来业界和研究者提出了基于编排(choreography)的新型服务组合构建思路。其基本想法是首先在全局观点下描述分布在网络上一组独立服务之间的组合和协作，然后自动生成各个局部的实现(框架)。针对这一领域的关键问题，本文提出了一个模型编排语言Chor，给出了它的形式化语法和语义，证明了编排的无死锁特性。为研究编排的实现，本文提出投影的概念，给出从全局编排模型到局部实现模型的投影法则，提出了编排的可实现性条件。在此基础上提出了一些支持编排描述的新语言结构及其投影实现规则：还实现了从WS-CDL编排到模型检查器SPIN的自动转换原型工具，以支持对编排的模拟和验证。 本文最后讨论了这一领域中的若干进一步研究问题。