Web服务的出现代表了分布式计算的最新要求。随着应用需要的不断提升,Web服务技术已从基础设施构建与概念推广阶段向大规模商业应用阶段快速发展,从而推动了支持B2B(business-to-business)和EAI(Enterprise Application Integration)的Web服务组合研究。本文通过剖析现有Web服务组合描述语言的结构组成,针对现有描述语言在形式化方面建模和验证的不足,利用分层Petri网作为形式化工具,对由WS-BPEL(WebServices Business Process Execution Language)描述的Web服务组合进行建模和验证。首先分析研究总结了常见的Web服务组合语言,对WS-BPEL结构和结构元素进行分类。在此基础上,给出了一个完整的利用分层Petri网对由WS-BPEL描述的Web服务组合进行建模的方法和过程。分层Petri网具有严密的数学基础,提供了一种有效的手段去模拟、分析和验证WS-BPEL流程,可以帮助对所生成的网模型进行验证。同时,在利用分层Petri网建模过程中采用巴克斯范式对WS-BPEL结构元素描述,总结提出了行之有效的化简规则、方法,便于简化模型。文章还对相应辅助工具的设计开发进行了介绍,以帮助上述建模过程的自动生成。