近年来，业务流程的广泛使用极大的提高了企业的生产效率，增加了企业的核心竞争力。但随着社会的不断发展，企业的业务目标也在不断调整，对业务流程的柔性调整的要求也越来越高。目前BPEL作为一种IT级业务流程的执行语言正在得到越来越广泛的应用，但由于BPEL流程是一种实现层语言，对于普通业务用户难以理解。本文前期提出了一种基于模板的业务流程到BPEL流程的转换方法，但是转换的过程是否正确，需要依托数学模型进行方法验证。　　 针对上述问题，本文在深入分析国内外研究现状基础上，开展了流程功能性验证的相关研究，基于Petri网理论、模态逻辑的互模拟等理论，提出了完整的BPEL流程功能一致性验证方法，本文的主要工作和贡献包括：　　 1.提出了业务流程到Petri模型的建模方法以及对BPEL建模方法的改进。　　 业务流程建模方法主要对业务流程活动节点，逻辑节点，事件节点，状态节点等类型都分别找到在Petri网中的对应关系，这种对应关系既符合Petri网的结构特征，又便于以后的化简和模型验证。BPEL流程建模方法通过分析调研目前对BPEL流程的建模方法，找出目前建模方法中的不足，对不足的原因进行了研究，提出了流程结构转换的解决方法对现有方法进行改进。　　 2.提出了Petri模型的化简方法并给出化简规则。　　 该方法定义了Petri模型的最简模型，最简模型以利于模型比较为原则。化简方法的核心在于定义Petri模型的化简规则，提出了一般Petri模型的化简规则，并且针对BPEL流程的语义性质，提出了专门的化简规则，并借助理论进行了证明，保证了利用规则化简后模型的一致性。　　 3.提出了BPEL流程功能-致性验证方法并设计实现了软件工具。　　 该方法以模态逻辑和时态逻辑的相关理论为基础，定义了流程结构和活动变迁执行顺序为互模拟中的二元关系，完成两个Petri模型之间的状态对应，通过Petri模型间的互模拟实现两个Petri模型的一致性验证。同时，实现了一个基于此方法的软件工具，该软件工具提供了友好的图形化操作界面，方便用户的对流程的构建、修改和验证。