随着Web服务技术的发展,网上发布的Web服务的数量将越来越多,当单个服务无法满足用户的需求时,需要将多个功能有限的服务进行服务组合,产生增值服务。手工地去组合这些Web服务,不便于对服务组合依据用户需求变化,进行动态调整,所以迫切需要对这些服务进行动态组合。Web服务本体描述语言OWL-S所描述的Web服务流程,使得Web服务包含机器可读的语义信息,可以实现Web服务的自动发现、组合、执行和监控。但动态服务组合却是一个复杂而易错的过程,现有的组合规范缺乏有效的验证机制,因此需要建立Web服务组合的形式化描述模型,利用对形式化模型的分析,验证方法来检验Web服务动态组合的正确性和有效性。目前已有一些形式化验证方法,主要有基于进程代数、自动机和Petri网。但是进程代数和自动机方法只是停留在语法层面,对语义信息描述不够,且建模过程复杂,模型抽象,缺乏直观的图形表示。由于基本Petri网没有颜色和分层的概念,不能精确表达Web服务不同类型的数据,而且对于大规模复杂系统,容易出现状态空间爆炸问题。本文提出一种利用分层着色Petri网(HCPN)对以OWL-S描述的Web服务组合流程建模和验证的方法。首先研究基于OWL-S的语义Web服务动态组合流程,得到Web服务组合过程模型;然后提出OWL-S描述的Web服务组合流程中的原子过程,复合过程以及各控制结构向Petri网转化的规则,得到Web服务动态组合过程模型对应的分层着色Petri网模型;最后利用CPN Tools工具对建立的CPN模型进行动态模拟仿真,并通过状态空间机制验证模型的有界性、可达性、活性(探测有无死锁)等各项性能。从而达到验证Web服务组合正确性和有效性的目的。分层着色Petri网(HCPN)建模,弥补了一般Petri网的不足,引入不同颜色的token以及token数的变化来表示OWL-S模型中的IOPE,可以更好的刻画Web服务的控制流和数据流,引入分层概念,可以简化模型,对于大型复杂系统可以分成一些子网,每个阶段独立验证,逐步求精,对于有相同结构的子网,不必重复建模。同时也有利于避免状态空间爆炸问题。