ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2005, Vol. 42 ›› Issue (1): 1-9.

• •    下一篇

工作流过程建模中的形式化验证技术

周建涛1,2 史美林1 叶新铭2   

  1. 1(清华大学计算机科学与技术系 北京 100084) 2(内蒙古大学计算机学院 呼和浩特 010021) (zjtao@csnet4.cs.tsinghua.edu.cn)
  • 出版日期: 2005-01-15

Formal Verification Techniques in Workflow Process Modeling

Zhou Jiantao1,2, Shi Meilin1, and Ye Xinming2   

  1. 1(Department of Computer Science & Technology, Tsinghua University, Beijing 100084) 2(College of Computer Science, Inner Mongolia University, Huhhot 010021)
  • Online: 2005-01-15

摘要: 工作流过程建模是一个复杂且易错的过程.若过程定义在投入运行之后被发现有错,则修复错误的代价相当高,这个问题引起了研究界和工业界的高度重视.因此,在建模阶段进行有效的过程验证是十分必要的.综述了工作流过程验证技术的发展现状,包括强调验证的重要性,叙述了需要验证的问题和复杂度;介绍了对验证方法的要求;讨论了过程合理性验证和化简验证技术等;并通过对研究现状的分析和对比,提出了仍然没有解决的问题和将来的工作.

关键词: 工作流, 过程建模, 验证, Petri网, 合理性, 化简

Abstract: Workflow process modeling is a complicated and error-prone procedure. It is highly noted in both research and industrial area that the cost for modifying errors is very high after a process definition becomes operational. Thus, effective process verification in modeling phase is very essential. This paper summarizes the state of the art of workflow process verification. Firstly, importance of verification is emphasized, then depiction of problems needed to be verified and their complexities are stated, next the requirements for verification methods are described. After introduction of these essential problems, two sorts of important verification techniques are discussed in detail. The first one is soundness verification, whose research results on Petri net model are presented. The second one is reduction verification, whose research results on Petri net and workflow graph are given. Besides, other verification methods, including correctness verification and those methods based on LTS or UML, etc. are simply mentioned. By analysis and comparison, the problems may be researched and future trends are finally presented.

Key words: workflow, process modeling, verification, Petri net, soundness, reduction