● 摘要
Web服务（Web Services）是一种新兴的技术，它在面向互联网的开发，部署和整合方面有着非常广阔的应用前景。Web服务实现了一种面向服务的体系架构（Service-Oriented Architecture），其中，各个功能被组织为多个自治并且能够互相协作的组件。这样的一个具有很强可重用性的组件也被称作为一个Web服务。在分布式、异构并且开放的系统中，构建语义Web服务组合是一个具有挑战性的问题，为了实现Web服务的分解，很多种方法都被采用过。其中，BPELWS （Business Process Execution Language Web Service，Web服务业务过程执行语言）已经成为了Web服务组合领域目前的标准。 相比于关注Web服务的具体实现，学者们对于研究Web服务行为及Web服务组合的建模与分析技术有着更浓厚的兴趣。而对于语义Web服务组合的形式化描述是一个非常重要的环节，因为开发出一个能够从任何抽象模型中剥离出来的系统建模方法，从而使其结构变得更清晰，可以帮助我们在对一个Web 服务系统仿真及形式化分析时有更好的整体性理解。 这篇论文首先回顾了关于Web服务及语义Web服务组合方面的一些里程碑式的概念和标准。我们调研了在文献中出现的Web服务组合建模与验证时采用的一些形式化方法，然后基于一些特性对这些形式化方法进行了比较。之后我们实现了一个系统模型，该模型基于染色Petri网算法（colored Petri-nets algorithm），通过图形表示方法提升了模型的表现力。最终我们基于一个案例验证了该方法的有效性。