近年来信息技术迅猛发展,很多的信息管理领域得到发展并不断壮大。电子商务、电子政务、办公自动化和企业信息系统的应用成为了当今管理信息系统应用的热点。在这些领域中,业务流程管理(Business Process Management,简称BPM)是它们共同关心的问题。当前,BPM主要依赖于工作流管理系统,但是当前的工作流管理系统在流程模型的验证方面还存在着较大的不足,也没有统一的标准。为了构建与JBPM(Java Business Process Management)工作流流程定义结构等价的Petri net模型,把工作流模型的属性分为隐性的和显性的,去除了那些与运行结构无关的因素,为模型转化提供了便利。为了满足对应的WF-net的soundness属性,修正了JBPM中负责工作流运行的模块。以JBPM的流程模型定义为基础,给出了在运行结构等价的前提下,将JBPM流程模型转化为WF-nets的转化规则。这其中涉及到对JBPM流程模型的子结构抽取、结构分类和子结构的Petri net建模。根据WF-nets的soundness属性,给出了JBPM过程模型正确性的验证指标和验证方法。分析了一类流程模型性质——选择自由性,这个性质保证了对应的WF-net模型满足soundness属性,最后给出了对JBPM的实现修正。