随着互联网技术与应用的迅速发展，Web服务作为一种新兴的Web应用模式及远程访问标准，很好地解决了异构平台上的数据和应用的整合与共享问题。但是，传统的Web服务缺乏语义信息，语义Web使得网络中的所有信息都是有语义的，使计算机能够理解和处理。语义Web技术和Web服务的结合产生了语义Web服务。语义Web服务使用无二义性、且计算机可以理解的语言来描述Web服务，对Web服务的自动发现、组合和调用提供了支持。　　 对语义Web服务组合进行形式化描述、分析和验证是检测Web服务的自动发现、组合和执行等问题的有效手段。本文在对现有的Web服务组合方法分析之后，依据语义Web服务的特点，提出了有色Petri网的语义Web服务组合形式化模型，形式化描述OWL-S中ServiceModel的6种基本的Web服务组合单元，并利用可达图及CTLMC工具对构造出的组合网模型进行正确性(可达性、活性、有效性和安全性等方面)验证。最后，通过具体实例演示语义Web服务组合的Petri网建模及验证过程，说明了所提方法的可行性与有效性。