近年来Web服务的理论和技术取得了长足的发展,其保证互操作性的协议栈下层在学术界和工业界已基本达成一致.然而Web服务的价值在于服务重用,新兴的Web服务组合正是主要的重用手段。然而基于流程的Web服务组合建模是一个复杂且易出错的过程。如果流程定义在投入运行之后被发现有错,则修复错误的代价相当高,因此,在建模阶段进行有效的过程验证时十分必要的。此外Web服务组合可能存在不必要的流程设计而影响执行效率。本课题提出一个基于Petri网的Web服务组合验证及简化方法,此方法包含建模、验证、简化三个阶段。首先以Petri网结合工作流模式建模Web服务组合;然后根据Petri网的三种性质(可达性,安全性以及死锁)定义出Web服务组合结构正确性验证模型并验证Web服务组合,最后运用流程简化规则简化Web服务组合。在具体实现上,本课题通过把BPEL文件转换成PNML文件来完成Web服务组合的Petri-Net建模;再分别以覆盖树、关联矩阵和状态方程,以及迁移矩阵等分析方法验证PNML文件的上述三项Petri-Net性质。最后以Web服务组合代数方法结合简化规则简化BPEL文件。