随着Internet在全球的发展，基于网络的分布式应用越来越呈现出多样性和复杂性。其中，统一的服务注册、发现、绑定和集成机制，成为广域环境中实现互操作的一种有效方式，并得到学术界和产业界的广泛认可。单个的Web服务能够提供的功能的有限性使得将共享的Web服务组合起来，以提供功能更为强大的服务成为必要，这促使Web服务组合研究的兴起。服务组合的结果表现为一个自动执行的处理流程。协调一个流程中服务调用的顺序、对服务之间的数据流进行管理，都需要提供有效性、可靠性和可度量性的支持。如何利用工具对Web服务组合进行建模，进而进行分析、验证和仿真成为当前急待解决的问题。 针对上述问题本文选用Petri 网作为服务组合的建模和验证工具。Petri网是一个图形化的数学建模工具。一方面利用图形化方式来描述流程，另一方面利用其形式化分析技术对所建立模型的正确性进行分析验证。本文以颜色Petri网为基础进行扩展，提出了一种基于扩展颜色Petri网的服务组合逻辑模型的构建方法。在这个方法中，设计了一个包括静态和动态两个方面的元模型，利用元模型的这两个方面的一致性，解决了服务组合过程中控制流、数据流、以及特殊的I/O流无法在同一个图中表示的问题。在验证方面，本文在Petri网已有性质和验证方法的基础上，采用图形和线性代数技术分析和验证了基于Petri网的服务组合逻辑应包含的性质：可达性、有界性、活性和互斥性。最后给出了全部性质验证过程及其重要步骤地实现的算法，以及对实验数据、平台和结果的分析。对这些理论和实验的总结为进一步的研究扩展打下了良好的基础。