电子学报

• 学术论文 •    下一篇

一种基于资源约束的工作流建模及分析方法

庞善臣1,2   

  1. 1. 山东科技大学信息科学与工程学院, 山东青岛 266590;
    2. 清华大学计算机科学系, 北京 100084
  • 收稿日期:2011-08-26 修回日期:2011-11-10 出版日期:2012-08-25
    • 作者简介:
    • 庞善臣 男,1974年出生于山东嘉祥.中国计算机学会Petri网专业委员会副主任,中国计算机学会服务计算专业委员委员,2008年同济大学计算机软件与理论专业博士毕业,研究方向包括Petri网理论与应用、服务计算、可信计算、分布式并发系统分析与验证等. E-mail:shanchenpang2008@gmail.com
    • 基金资助:
    • 国家973重点基础研究发展规划 (No.2010CB328105); 国家自然科学基金 (No.60970001,No.91018007,No.61170183); 山东省优秀中青年科学家科研奖励基金 (No.BS2011SW025,No.BS2011DX027)

Modeling and Verification of Workflow Based on Resource Constraint

PANG Shan-chen1,2   

  1. 1. College of Information Science & Engineering, Shandong University of Science & Technology, Qingdao, Shandong 266590, China;
    2. Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
  • Received:2011-08-26 Revised:2011-11-10 Online:2012-08-25 Published:2012-08-25
    • Supported by:
    • National Program on Key Basic Research Project of China (973 Program) (No.2010CB328105); National Natural Science Foundation of China (No.60970001, No.91018007, No.61170183); Scientific Research Award Fund for Outstanding Young and Middle-aged Scientists of Shandong Province (No.BS2011SW025, No.BS2011DX027)

摘要: 资源约束是工作流正确实施的一个瓶颈问题,因此工作流系统的资源建模及模型正确性验证方法显得非常重要.为此,基于Petri网和工作流建模方法,提出了一种资源约束的工作流系统的形式化建模和分析技术,定义了资源空间(RS)、资源子网、资源工作流网和资源工作流网完整性(soundness)的概念,建立了资源调用视图以及Petri网影射模型,得到了资源工作流网保持完整性判定的一个充要条件.该方法将系统资源建模和过程建模合成到一个模型中,解决了工作流系统资源和过程分别建模给系统的正确性验证带来的困难,为工作流系统资源状态的可视化和进行有效的系统验证提供了模型依据.给出的实例验证了模型的有效性.

关键词: 资源约束, 工作流网, 资源子网, 资源工作流网, 完整性

Abstract: Resource constraint is a choke point of workflow system,and the efficient resource modeling and Verification methods are more important for workflow management system(WFMS).A new formal method used to model and analyze workflow system with resource constraint,resource workflow net,is presented based on Petri net and workflow techniques in this paper.Based on the definition of resource space(RS),resource subnet,resource workflow net(RWF-net),and soundness of the RWF-net,the resource scheduling views model formulated in WFMS are described and translated into Petri net,and a necessary and sufficient condition for the soundness of RWF-net is presented.The method integrate process model and resource model that can solve system analysis and verification problem for the process and resource modeled respectively and assure the consistency between process model and resource model. The usability of the research results in this paper is illustrated by an example.

Key words: resource constraint, workflow net, resource subnet, resource workflow net, soundness

中图分类号: