Web服务组合解决了互联网异构应用的集成和协作问题。Web服务组合建模是一个复杂且易出错的过程。如果组合流程在投入运行后被发现有错,则修复错误的代价很高,而且流程结构的正确性直接关系到业务集成的效率。因此对服务组合BPEL流程结构的正确性验证是Web服务组合研究领域的重要问题。目前这方面的研究仅限于理论层面,缺少切实可行的流程验证工具。本文提出了基于Petri网的BPEL流程调试工具,利用Petri网的改进形式PNBP(Petri-Net for BPEL Process)模型对流程建模,实现了BPEL流程的逻辑验证和流程仿真,主要工作如下:(1)在对Petri网理论分析的基础上,提出了针对BPEL流程的Petri网——PNBP模型的定义,利用PNBP模型对BPEL流程的顺序活动、并发活动、选择活动和循环活动进行了建模,从而实现任意结构的BPEL流程建模。(2)采用覆盖树、关联矩阵和状态方程、迁移矩阵对BPEL流程建模后的模型进行了安全性、可达性和死锁性质验证。(3)设计并实现了调试工具,重点对BPEL文件向PNML(Petri Net MarkupLanguage)文件的转化、PNML文件的解析及流程的逻辑验证部分从实现上进行了详细分析。通过贷款审批案例的调试演示了BPEL流程的建模、验证和仿真过程,说明了本文研究的调试工具的实用性和易用性。该工具已经在国家高技术发展计划项目“高可信的软件生产线”子课题“面向流程管理的软件生产线”中得到了运用。