基于Petri网的工作流模型验证
摘要
工作流过程建模是一个复杂且容易出错的过程。目前对工作流模型的验证与分析还是一个比较薄弱的环节,若过程定义在投入运行之后被发现有错,则修复的代价是相当高的。因此,在建模阶段进行有效的过程验证是非常有必要的。特别是最近几年,工作流技术在业务过程重组(Business Process Re-engineering BPR)中的作用更为突出,对复杂流程的分析与验证研究的需求也越来越迫切。完善工作流过程建模理论已经成为工作流管理系统的一个重要发展方向。
本文主要研究基于Petri网的工作流模型验证方法,并将验证方法适用于JBOSS JBPM建立的工作流管理系统。
本文首先在参考了大量工作流系统研究的基础上,利用Petri网结构分析理论,分析了现有合理性验证方法的优点以及不足,然后根据工作流网的特点,给出符合自由选择网结构的工作流网的合理性验证方法。
论文在第四章介绍了JBOSS JBPM工作流管理系统。JBPM是一个基于J2EE的轻量级的工作流管理系统。JBPM是开源项目,它的一个最大特色就是采用了自己定义的流程定义语言(JPDL),在详细分析JPDL的基础上,给出了将JPDL映射为Petri网的算法,以方便运用Petri网的验证方法。
论文最后将本文提出的工作流合理性验证方法运用于JBPM建立的工作流系统上,以验证方法的实用性。
The modeling of a workflow process is a complicated and error-prone procedure. However, the process verification in modeling phrase is comparatively weak at present. The cost will be very high if errors are found after the workflow is carried out in practice; therefore, the process verification is essential in the modeling of workflow phrase. Especially in recent years, with workflows plays a more and more important role in business process reengineering, there is an urgent demand for verification research and analysis of complex process. Therefore, to improve the model theory has become an important research direction.
The dissertation tries to make contributions to the research of workflow verification; the research is focused on Petri Nets analysis theories. In order to demonstrate the theory the dissertation proposed, it is applied to a JBPM workflow management system.
By studying many available researches on workflow verification and using the Petri theory on structural and behavioral properties, the dissertation analyses the good qualities and defects of the available achievements, and proposes an algorithm for the soundness of the workflow model according to the characteristics of Wfnet. JBOSS JBPM management system is introduced in Chapter 4 of the dissertation.
JBPM is an open source and lightweight workflow management system. The most important feature of JBPM is JPDL; JPDL is a process language to implement BPM and workflow in java. An algorithm for mapping JPDL to Petri Nets is given on the basis of Alast’s task structure and JPDL language, it will facilitate the use of Petri Nets in workflow model verification process.
A JBPM instance is made in the end of the dissertation, the instance attempt to demonstrate the right and soundness of the theory proposed in chapter 3 and chapter 5 of the dissertation.
本文主要研究基于Petri网的工作流模型验证方法,并将验证方法适用于JBOSS JBPM建立的工作流管理系统。
本文首先在参考了大量工作流系统研究的基础上,利用Petri网结构分析理论,分析了现有合理性验证方法的优点以及不足,然后根据工作流网的特点,给出符合自由选择网结构的工作流网的合理性验证方法。
论文在第四章介绍了JBOSS JBPM工作流管理系统。JBPM是一个基于J2EE的轻量级的工作流管理系统。JBPM是开源项目,它的一个最大特色就是采用了自己定义的流程定义语言(JPDL),在详细分析JPDL的基础上,给出了将JPDL映射为Petri网的算法,以方便运用Petri网的验证方法。
论文最后将本文提出的工作流合理性验证方法运用于JBPM建立的工作流系统上,以验证方法的实用性。
The modeling of a workflow process is a complicated and error-prone procedure. However, the process verification in modeling phrase is comparatively weak at present. The cost will be very high if errors are found after the workflow is carried out in practice; therefore, the process verification is essential in the modeling of workflow phrase. Especially in recent years, with workflows plays a more and more important role in business process reengineering, there is an urgent demand for verification research and analysis of complex process. Therefore, to improve the model theory has become an important research direction.
The dissertation tries to make contributions to the research of workflow verification; the research is focused on Petri Nets analysis theories. In order to demonstrate the theory the dissertation proposed, it is applied to a JBPM workflow management system.
By studying many available researches on workflow verification and using the Petri theory on structural and behavioral properties, the dissertation analyses the good qualities and defects of the available achievements, and proposes an algorithm for the soundness of the workflow model according to the characteristics of Wfnet. JBOSS JBPM management system is introduced in Chapter 4 of the dissertation.
JBPM is an open source and lightweight workflow management system. The most important feature of JBPM is JPDL; JPDL is a process language to implement BPM and workflow in java. An algorithm for mapping JPDL to Petri Nets is given on the basis of Alast’s task structure and JPDL language, it will facilitate the use of Petri Nets in workflow model verification process.
A JBPM instance is made in the end of the dissertation, the instance attempt to demonstrate the right and soundness of the theory proposed in chapter 3 and chapter 5 of the dissertation.
引文
[1] W.M.F. van der Alast, K van Hee.王建民,闻立杰等译.工作流管理—模型、方法和系统[M],北京:清华大学出版社, 2004
[2] LING Hong, ZHOU Jiang Bo. Research on workflow process structure verification [C], IEEE International Conference on e-Business Engineering, 2005.
[3] Sinnakkrishnan Perumal, Ambuj Mahanti. A Graph-Search Based Algorithm for Verifying Workflow Graphs [C], the 16th International Workshop on Database and Expert Systems Applications, 2005.
[4] J.-H. Pfeiffer, W.R. Rossak, A. Speck. Applying Model Checking to Workflow Verification [C], the 11th International Conference and Workshop on the Engineering of Computer-Based Systems, 2004
[5]范玉顺.工作流管理技术基础[M],北京:清华大学出版社,施普林格出版社,2001
[6] Workflow Management Coalition Workflow Standard. Workflow Process Definition Interface–XML process Definition Language [S]:2002.10.
[7]周建涛,史美林,叶新铭.一种基于Petri网化简的工作流过程语义验证方法[J],软件学报, 2005,16(7):1242～1251.
[8]赵文,袁崇义,刘刚,张世琨,王立福.基于P/T系统化简方法的工作流过程模拟验证[J],软件学报,2004,15(10):1423～1430.
[9] W.M.P van der Alast. Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques[R], Berlin:Springer-Verlag,2000.161～183.
[10]陈翔,夏国平,李涛.基于Petri网的工作流模型合理性研究[J].北京理工大学学报.2004, 24(12), 1074～1078.
[11] W.M.F van der Alast. Verification of workflow nets[R], In: P.Azéma,editor,Application and Theory of Petri Nets,Lecture Notes in Computer Science 1248, Berlin, Springer-Verlag,1997: 407～426.
[12]唐邦志,魏生民,景韶宇,周欣.工作流网XPDL映射[J],计算机工程与应用,2003,36(04): 41～44.
[13] W.M.F. van der Alast, A.H.M ter Hofstede. Verification of Worklflow Task Structures: APetri-net-based approach[J], Information System, 2000, 25(1):43～69.
[14]吴振寰,王鹏伟. Petri网关联矩阵与PNML描述之间的转换[J],计算机工程与应用,2006, 21(03),32～34.
[15]胡长城.工作流引擎核心调度算法与Petri Net[EB/OL], http://www.javafox.org, 2005.04.17.
[16] K.S.Cheung. use-case-driven system design: a synthesis methodology based on labeled Petri Nets [D], Dept of Computer Science, City University of HongKong, 2002.
[17] W.M.P van der Alast. Structural Characterization of Sound Workflow nets [C], Computing Science Report 96/23, Eindhoven University of Technology, Eindhoven, 1996.
[18] W.M.P van der Alast. The Application of Petri nets to Workflow Management[J], The Journal of Circuit,System and Computers,1998,8(1):21～66.
[19] W.M.P van der Alast. Verification of workflow nets [J], in proceeding of 18th internation conference, ICATPN’97: Toulouse, France;23～27 Jun 1997.
[20] P.Aaema and G.Ballbo, Eds.. Lecture notes in Computer Science[J], Application and theory of Petri nets, 1997, 1248, 407～426.
[21]李建强,范玉顺.基于Petri网化简方法的工作流模型验证[J],信息与控制,2001,30(6): 493～497.
[22] W.M.P van der Alast,Arthur H.M. ter Hofstede. Verification of Workflow Task Structure:A Petri-Net-Based Approach[J],Information system,2000,25(1):43～69.
[23] Qu Y, Lin C, Marinescu D C. Workflow model: From process Algebra to Petri net[C]. Submitted to 23rd International Conference on Conceptual Modeling, April, 2004.
[24] Lin C, QU Y. Temperal Inference of Workflow systems Based on Time Petri nets[J]: Quantitative and Qualitative Analysis. International Journal of Intelligent Systems, 2004,19(5):417～442.
[25]Li Hui Fanf, Fan Yu Shun. Workflow Model Analysis Based on Time Constrant Petri Nets [J], Journal of Software, 2004, 15(01), 17～26.
[26]杜淑楠,章宁,王鲁滨.工作流模型正确性验证过程中的模型化简问题[J],计算机工程, 2005,7(31),110～114.
[27] W.Sadiq, M.E.Orlowska. Applying graph reduction techniques for identifying structural conflicts in process models[R], In M. Jarke , A.Oberweis,editors,Proceeding of the 11thInternational Conference on Advanced Informatin System Engineering(Caise’99), Lecture Nodes in Computer Science 1626,Berlin,Springer-Verlag,1999:195209.
[28] W.Sadiq, M.E.Orlowska. Analyzing process models using graph reduction techniques [J], Information System, 2000, 25(2):117～134.
[29]罗海滨,范玉顺,吴澄.工作流合理性验证中的时间平衡分析[J],软件学报,2002, 13(08): 1686～1691.
[30]赵磊,钱乐秋,赵文耘.基于状态空间的工作流模型验证[J].计算机工程与应用.2004, 220～222
[31]邹宇,刘毅,陈佩文.基于图归约法的工作流模型验证[J].计算机应用.2003, 23(4),86～88
[32] W.M.P. van der Alast and K.M.van Hee. Business Process Redesign: A Petri-Net-Based Approach[J]. Computers in Industry 29, 1996, 1(2): 15 ~26.
[34] Clarke E M, Grumberg O, Peled D. Model checking[M]. Cambridge, MA: MIT Press, 1999.
[35]曲扬.基于Petri网的工作流建模和分析方法研究[D].清华大学,2004.
[36] JBPM官方网站[EB/OL]: http://www.jboss.com/products/jbpm.
[37] JBPM JPDL User Guide[EB/OL]: http://docs.jboss.com/jbpm/v3.2/userguide/html.
[38] JBPM Workflow Management [EB/OL], http://hi.baidu.com/daomeidigua/blog/item/0f59edc4d03e9da98226acd9.html
[39]许宏图,赵政.基于JBPM的协同软件的研究[J],计算机技术与发展,2006,8(16),16～20.
[40] Hibernate官方文档[EB/OL],http://www.hibernate.org.
[41] Alur,Deepak Malks, Dan Crupi, John. Core J2EE Patterns[J],Person Education,2003,550～572.
[42] JDOM详解[EB/OL]: http://www.webdn.com/web_file/3sword/xml/0602016011.
[43]谢艳平,胡家宝.基于J2EE和Jbpm的分布式工作流的研究与应用[D],2006.04.
[44]施发健,赵政. JBPM-工作流项目的研究与实践[D],2005.05.
[45]王亚沙,何晓阳,赵俊峰.一种支持构件化过程开发方法和分级管理机制的过程管理工具[J],小型卫星计算机系统,2006,3(27):469～473.
[2] LING Hong, ZHOU Jiang Bo. Research on workflow process structure verification [C], IEEE International Conference on e-Business Engineering, 2005.
[3] Sinnakkrishnan Perumal, Ambuj Mahanti. A Graph-Search Based Algorithm for Verifying Workflow Graphs [C], the 16th International Workshop on Database and Expert Systems Applications, 2005.
[4] J.-H. Pfeiffer, W.R. Rossak, A. Speck. Applying Model Checking to Workflow Verification [C], the 11th International Conference and Workshop on the Engineering of Computer-Based Systems, 2004
[5]范玉顺.工作流管理技术基础[M],北京:清华大学出版社,施普林格出版社,2001
[6] Workflow Management Coalition Workflow Standard. Workflow Process Definition Interface–XML process Definition Language [S]:2002.10.
[7]周建涛,史美林,叶新铭.一种基于Petri网化简的工作流过程语义验证方法[J],软件学报, 2005,16(7):1242～1251.
[8]赵文,袁崇义,刘刚,张世琨,王立福.基于P/T系统化简方法的工作流过程模拟验证[J],软件学报,2004,15(10):1423～1430.
[9] W.M.P van der Alast. Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques[R], Berlin:Springer-Verlag,2000.161～183.
[10]陈翔,夏国平,李涛.基于Petri网的工作流模型合理性研究[J].北京理工大学学报.2004, 24(12), 1074～1078.
[11] W.M.F van der Alast. Verification of workflow nets[R], In: P.Azéma,editor,Application and Theory of Petri Nets,Lecture Notes in Computer Science 1248, Berlin, Springer-Verlag,1997: 407～426.
[12]唐邦志,魏生民,景韶宇,周欣.工作流网XPDL映射[J],计算机工程与应用,2003,36(04): 41～44.
[13] W.M.F. van der Alast, A.H.M ter Hofstede. Verification of Worklflow Task Structures: APetri-net-based approach[J], Information System, 2000, 25(1):43～69.
[14]吴振寰,王鹏伟. Petri网关联矩阵与PNML描述之间的转换[J],计算机工程与应用,2006, 21(03),32～34.
[15]胡长城.工作流引擎核心调度算法与Petri Net[EB/OL], http://www.javafox.org, 2005.04.17.
[16] K.S.Cheung. use-case-driven system design: a synthesis methodology based on labeled Petri Nets [D], Dept of Computer Science, City University of HongKong, 2002.
[17] W.M.P van der Alast. Structural Characterization of Sound Workflow nets [C], Computing Science Report 96/23, Eindhoven University of Technology, Eindhoven, 1996.
[18] W.M.P van der Alast. The Application of Petri nets to Workflow Management[J], The Journal of Circuit,System and Computers,1998,8(1):21～66.
[19] W.M.P van der Alast. Verification of workflow nets [J], in proceeding of 18th internation conference, ICATPN’97: Toulouse, France;23～27 Jun 1997.
[20] P.Aaema and G.Ballbo, Eds.. Lecture notes in Computer Science[J], Application and theory of Petri nets, 1997, 1248, 407～426.
[21]李建强,范玉顺.基于Petri网化简方法的工作流模型验证[J],信息与控制,2001,30(6): 493～497.
[22] W.M.P van der Alast,Arthur H.M. ter Hofstede. Verification of Workflow Task Structure:A Petri-Net-Based Approach[J],Information system,2000,25(1):43～69.
[23] Qu Y, Lin C, Marinescu D C. Workflow model: From process Algebra to Petri net[C]. Submitted to 23rd International Conference on Conceptual Modeling, April, 2004.
[24] Lin C, QU Y. Temperal Inference of Workflow systems Based on Time Petri nets[J]: Quantitative and Qualitative Analysis. International Journal of Intelligent Systems, 2004,19(5):417～442.
[25]Li Hui Fanf, Fan Yu Shun. Workflow Model Analysis Based on Time Constrant Petri Nets [J], Journal of Software, 2004, 15(01), 17～26.
[26]杜淑楠,章宁,王鲁滨.工作流模型正确性验证过程中的模型化简问题[J],计算机工程, 2005,7(31),110～114.
[27] W.Sadiq, M.E.Orlowska. Applying graph reduction techniques for identifying structural conflicts in process models[R], In M. Jarke , A.Oberweis,editors,Proceeding of the 11thInternational Conference on Advanced Informatin System Engineering(Caise’99), Lecture Nodes in Computer Science 1626,Berlin,Springer-Verlag,1999:195209.
[28] W.Sadiq, M.E.Orlowska. Analyzing process models using graph reduction techniques [J], Information System, 2000, 25(2):117～134.
[29]罗海滨,范玉顺,吴澄.工作流合理性验证中的时间平衡分析[J],软件学报,2002, 13(08): 1686～1691.
[30]赵磊,钱乐秋,赵文耘.基于状态空间的工作流模型验证[J].计算机工程与应用.2004, 220～222
[31]邹宇,刘毅,陈佩文.基于图归约法的工作流模型验证[J].计算机应用.2003, 23(4),86～88
[32] W.M.P. van der Alast and K.M.van Hee. Business Process Redesign: A Petri-Net-Based Approach[J]. Computers in Industry 29, 1996, 1(2): 15 ~26.
[34] Clarke E M, Grumberg O, Peled D. Model checking[M]. Cambridge, MA: MIT Press, 1999.
[35]曲扬.基于Petri网的工作流建模和分析方法研究[D].清华大学,2004.
[36] JBPM官方网站[EB/OL]: http://www.jboss.com/products/jbpm.
[37] JBPM JPDL User Guide[EB/OL]: http://docs.jboss.com/jbpm/v3.2/userguide/html.
[38] JBPM Workflow Management [EB/OL], http://hi.baidu.com/daomeidigua/blog/item/0f59edc4d03e9da98226acd9.html
[39]许宏图,赵政.基于JBPM的协同软件的研究[J],计算机技术与发展,2006,8(16),16～20.
[40] Hibernate官方文档[EB/OL],http://www.hibernate.org.
[41] Alur,Deepak Malks, Dan Crupi, John. Core J2EE Patterns[J],Person Education,2003,550～572.
[42] JDOM详解[EB/OL]: http://www.webdn.com/web_file/3sword/xml/0602016011.
[43]谢艳平,胡家宝.基于J2EE和Jbpm的分布式工作流的研究与应用[D],2006.04.
[44]施发健,赵政. JBPM-工作流项目的研究与实践[D],2005.05.
[45]王亚沙,何晓阳,赵俊峰.一种支持构件化过程开发方法和分级管理机制的过程管理工具[J],小型卫星计算机系统,2006,3(27):469～473.