基于Petri网工作流模型的分析(doc 10页)
西北大学学报(自然科学网络版) 2004年5月，第2卷，第5期
Science Journal of Northwest University Online May 2004，Vol.2，No. 5
基于Petri网工作流模型的分析
晋 蓓，冯卫兵
（1. 西北大学 计算机科学系，陕西 西安 710069；2. 西安科技大学 基础部，
陕西 西安 710054）
摘要：通过模型分析发现所描述的过程定义中的设计错误，以便对业务过程重构提供正确的指导和科学的依据。首先将信牌驱动模型转化为Petri网，接着将Petri网进行必要化简，最后对化简后的Petri网进行死锁等分析。
关 键 词： 工作流模型；Petri网；死锁
________________________ 收稿日期：2004-02-03
审 稿 人：葛玮，男，西北大学计算机科学系副教授
中图分类号：TP911.7 文献标识码：A 文章编号：1000-274X(2004)0068-07
工作流模型的分析是指采用各种方法（包括理论模型、模拟、测量方法），对工作流模型的内部行为进行分析计算，使得工作流模型在理论上是正确和有效的。
虽然现在绝大部分的工作流产品都提供模型性能分析的仿真功能，但由于复杂性等原因，很难找到一种有效的算法对模型进行分析与验证。本文在总结模型分析研究成果现状的基础上，针对目前模型验证方法存在的不足，总结了Petri网模型分析中的一些图形化简规则，针对企业经营过程模型的特点并利用文中提出的模型
10
正确性标准，提出了一种具有完备性和高效率的工作流模型的模型验证方法分析。
1 相关概念
定义1 信牌驱动模型的静态结构: 多元式TP(A,T,F)(A,T;F,A,A,W,A0fSPLITJOIN,A,D)称为信牌驱动模型的静态结构（以下简称信牌驱动模型），其中：
1) D表示扩展的信牌驱动模型所
?表涉及的所有数据，其值域用D示； 2)
A表示活动集合，和G分别称为功能函数
2D?a?A,a?(G1,G2),G1和后继函数。G被定义为21?2D,G2根据
出函数定义，参见下边的定义；
3）T表示信牌箱集合；
4）F?T?A?A?T，称为TP的流关系，其中T?A和A?T分别称为入关系和出关
10
系。对出关系定义一个出函数FO：
A?T?D?TF。?A?A，FOA表示与A相关的出
函数，被称为A的后继函数。
5）
A0?A是惟一的活动，称为开
0始活动，*A6）
Af?A??；
是一个活动的集合，称
f为结束活动，A*??；
7） W:F?N称为转移的权重；
A8）是A（注意：A中不包含A,A）
SPLIT0f的一种划分
AAND?AOR?AXOR??,{AAND,AOR,AXOR},即
是A的另一种
，即规
定
AAND?AOR?AXOR?A,JOINA划分
OR{ANDA,ORA,XORA,asyncA,t-andA}A?ANDA?XORA?asyncA?t-andA??,A?ANDA?XORA?asyncA?t-andA?AOR。若*A?1，
AND则A?ANDA；若*A?1，则A?A；如
果*A?*A?1，则A被称为简单元素。
10
基于Petri网工作流模型的分析(doc 10页)
