近年来，Internet正由传统意义下的信息发布平台逐渐演变为一种特定形式的开放分布计算环境，越来越多的数据资源、计算资源与应用资源依托Internet成为可被公共访问和获取的网络资源。在开放的网络环境下实现跨组织的网络资源共享与应用集成已成为学术界和工业界具有广泛需求的基础性研究课题。随着Web服务技术的出现和推广，Web服务已成为公认的实现分布计算的主流技术选择。　　 基本Web服务是一种能够实现Internet上独立业务逻辑的服务，允许其他应用程序通过Internet连接并对其进行调用。然而基本Web服务的功能有限，Web服务组合可把多个基本Web服务组合为一种复杂应用，从而提供功能更为强大的增值服务。关于Web服务组合这一问题，目前已出现了多种Web服务组合建模语言，这些语言大都基于XML，虽然比较形象和直观，但是缺乏精确的语义，不利于对组合Web服务的一些性质进行严格的分析和验证。　　 针对上述问题，本文利用形式化方法对Web服务组合的建模和分析若干关键技术进行了研究，提出了一种基于Petri网的Web服务组合网，在此基础上，讨论了从两个不同的抽象层进行建模的Web服务组合语言到服务组合网的映射，并对映射结果进行了分析。主要内容包括：　　 1.提出了一种基于Petri网的Web服务组合网。基于现有的工作流元模型，结合Web服务组合的特点，提出了一种扩展的Web服务组合元模型。在此基础上，基于同步网，提出了一种分层的Web服务组合网（简称服务网，记为ServiceNet）。最后基于Web服务组合网，提出了一种Web服务组合模式的构造方法，结果证明Web服务组合网具有较强的表达能力。这一成果有助于基于形式化的理论与方法建立Web服务组合分析与验证工具，从而为组合Web服务的正确性提供保证。　　 2.提出了WS-BPEL和WS-CDL到ServiceNet的一组转换规则。Web服务业务流程执行语言WS-BPEL是基于编排（orchestration）的Web服务组合语言标准，已被广泛用于业务流程的实现。Web服务联编描述语言WS-CDL是基于联编（choreography）的Web服务组合语言标准，描述分布在网络上的一组独立Web服务之间的组合和协作。实际应用对WS-BPEL和WS-CDL程序的正确性提出了很高要求，为了更好地理解WS-BPEL语言和WS-CDL语言，并支持对WS-BPEL程序和规范及WS-CDL程序和规范的形式化验证，本文给出了WS-BPEL和WS-CDL到ServiceNet的转换规则，并定义了相应的语义。　　 3.定义了ServiceNet的相关性质并提出了相应的验证方法。畅通性是ServiceNet逻辑的一个重要性质，对于保证组合Web服务的正确运行至关重要。扩充了同步网逻辑的化简规则并提出了一种基于矩阵变换的ServiceNet逻辑畅通性验证方法。定义了访问无效数据和数据访问冲突两种数据流相关属性，并分别给出了它们的验证方法。WS-BPEL从编排观点描述组合Web服务的实现，而WS-CDL则从联编观点描述分布在网络上的多个Web服务之间的协作，提出了WS-BPEL和WS-CDL之间一致性的验证方法。以上研究工作可以用于验证WS-BPEL和WS-CDL所描述的服务组合是否存在本文提出的控制流和数据流错误，以及两种服务组合实现的一致性。　　 4.设计并实现了Web服务组合原型系统及相关工具。相关工具主要包括Web服务组合建模工具、WS-BPEL到ServiceNet的转换工具、WS-CDL到SetviceNet的转换工具，以及ServiceNet的分析与验证工具。