担保业务管理系统工作流的Petri网建模
开篇：润墨网以专业的文秘视角，为您筛选了一篇担保业务管理系统工作流的Petri网建模范文，如需获取更多写作素材，在线客服老师一对一协助。欢迎您的阅读与分享！
摘要：应用Petri网建模与工作流技术，构建了担保业务管理系统工作流的petri网模型，并对一个担保业务管理系统工作流实例，给出了基于Petri网化简分析方法的模型化简与性质验证，表明该模型能够对担保业务管理系统工作流进行有效的分析和验证，从而为担保业务管理系统工作流分析提供了理论基础。
关键词：Petri网；工作流；担保业务
中图分类号：TP311文献标识码：A文章编号：1009-3044(2008)32-1149-03
Petri-net-based Modeling for Surety Business Management System Workflow
ZHANG Xin-fang
(School of Computer Science & Technology, Soochow University, Suzhou 215500, China)
Abstract: This thesis has constructed a Petri-net model for Surety Business Management System Workflow, applying technology of Petri-net-based Modeling and Workflow. Model reduction and properties verification based on Petri net reduction are presented for a Surety Business Management system workflow instance. The research result indicates that this model can effectively analyze and verify a Surety Business Management workflow system. Thus it enriches theory on design and workflow analysis in Surety Business Management system integration.
Key words: petri-net; workflow; surety business
1 引言
担保行业是信息和知识应用高度密集型行业，其一系列行为都必须要建立在高质量信息平台的基础上。担保业务管理系统为信用担保机构提供业务工作平台，为担保业务各活动提供支持工具,便于决策层对各项业务指标进行全面监控，从而控制并降低担保风险。
担保业务流程本身的复杂性与对正确性的高度要求，需要一种形式化的建模和验证分析技术作为理论支撑。1962年德国的CA. Petri博士在研究自动机通信时，提出了一套形式化的建模方法，在当时引起了学术界的广泛关注，因此用他的名字命名为Petri网[1]。Petri网是一种系统建模与分析工具，它兼顾了严格语义与图形语言两个方面，是一种基于状态的建模方法，具有强有力的分析技术和手段[2,3]，因而非常适合于工作流建模及其分析。荷兰学者W.M.P. van der Aalst定义了基于Petri网的工作流系统的形式化模型――工作流网，并研究了基于工作流网的分析和验证技术，建立了网性质和工作流性质之间的对应关系，大大推动了基于Petri网的工作流建模及其分析等方面的工作[4]。
在上述工作的基础上，本文将工作流网模型应用到担保业务管理系统中，提出了担保业务管理系统工作流的建模方法，构建了担保业务管理系统工作流的形式化模型。基于该模型，就能对担保业务管理系统工作流进行有效的分析和验证。
2 相关理论
2.1 Petri网概述
首先，给出本文所需的Petri网的基本概述和定义，有关Petri网的详细资料可参考文献[5][6]。
经典Petri网是由矩形表示的变迁(Transition)和由圆圈表示的库所(Place)两种元素构成的有向图，转换和库所之间通过有向连接弧(Arc)连接。
定义2.1（Petri Net）一个Petri网是一个四元组，PN＝{P,T,F,W}，其中：
1) P＝{p1，p2，…，pn}是库所的有穷集合；
2) T＝{t1，t2，…，tm}是变迁的有穷集合；
3) F?哿(P×T)∪(T×P)是有限连接弧的有穷集合，表示库所与变迁之间的顺序关系；
4) W:F{1,2,3,…}是一个指定连接弧权重的函数；
5) P∪T≠Ф且P∩T=Ф。
如果从库所p到变迁t有一个连接弧，即∈F，则p称为t的输入库所。相反若从变迁t到库所p有一个连接弧，即∈F，则p称为t的输出库所。・t表示变迁t的所有输入库所的集合，t・表示变迁t的所有输出库所的集合。・p和p・也具有相应的含义，分别表示以库所p作为输入库所的变迁集合和以库所p作为输出库所的变迁集合。
在Petri网中，任何时刻每个库所都拥有零个或多个托肯（Token），托肯在各个库所间的分布状况代表着Petri网的状态（State，或Marking）。即Petri网的状态M∈P->IN，例如3p1＋0p2＋3p3＋1p4代表库所p1和p3拥有三个托肯，库所p4中有一个托肯，而库所p2则没有托肯。另一种表示方法是：3p1＋3p3＋1p4。为比较两种状态，通常会定义状态之间的偏序关系：对于Petri网PN的任意两个状态M1和M2，M1≤M2当且仅当对于每个p∈P有M1(p)≤M2(p)成立。
在Petri网的运行过程中，变迁按如下规则改变托肯在Petri网中分布情况：
1) Enable规则，一个变迁t有效（enabled）当且仅当t的每个输入库所p至少有w(p, t)个托肯，其中w(p, t)表示从p到t的连接弧的权重；
2) Fire规则，有效变迁可以被激发，变迁t激发的结果是从其输入库所p中删除w(p, t)个托肯，向其输出库所p中添加w(t, p)个托肯，其中w(t, p)表示从t到p的连接弧的权重。
对于Petri网PN＝｛P，T，F，W｝和状态M1，有如下标记：
2.2 工作流网
van der Aalst W M P在Petri网的基础上定义了工作流网(Workflow Net)。在工作流网中，库所对应过程中的条件，变迁对应过程中的可执行活动。
工作流网还要求有一个起始库所和一个终止库所，所以需在开始节点对应的变迁ti前增加起始库所i，并把i与ti通过连接弧连接。在过程模型中增加一个终止节点，所有结束节点都有一条无条件的路由边与该终止节点直接连接。该终止节点无具体业务功能，只是为了限制每个工作流网只有唯一的出口。每个结束节点执行结束后都会路由到该终止节点，然后整个流程终止。同时在终止节点to增加终止库所o，并把to与o通过连接弧连接。由此得到工作流网的定义。
定义2.2 (Workflow Net)一个Petri网PN=(P,T,F,W)是一个工作流网WN(Workflow Net)当且仅当下面三个条件成立：
1) PN有两个特殊的库所：i和o，其中库所i被称为源库所（source place），且・i＝?I，库所o被称为终止库所（sink place），且o・＝?I；
2) 当PN增加一个连接o和i的变迁后t*（即・t*＝｛o｝，t*・＝｛i｝），该Petri网是一个强连通Petri网；
3) 连接弧的权重都是1，即W：F->{1}。
条件1表示由工作流网WN表示的过程实例执行时有唯一入口和出口。条件2是为限制在工作流网WN中，不存在执行不到的变迁，即每个变迁对应节点对整个过程模型的执行都是有贡献的。条件3表示每个工作流网都是一个普通（ordinary）Petri网。在本文后续部分，如果没有特殊强调，Petri网中连接弧的权重都是1，Petri网用三元组（P，T，F）表示。
因为一条路由边只会连接一个源节点和一个目的节点，所以经路由边转化而得的库所都只有一个输入变迁和一个输出变迁。而且起始库所i没有输入变迁，唯一输出变迁是开始节点对应的变迁；终止库所o没有输出变迁，唯一的输入变迁是终止节点对应的变迁。所以工作流中每个库所最多只有一个输入变迁和一个输出变迁，因此工作流网又是一种加标图（marked graph）。
需要注意工作流网刻画的是单个过程实例的执行情况，而且定义5中的三个条件只是最小约束，这意味着即使满足这三个条件的工作流网在实际执行时仍可能出现死锁等错误情况。
每个工作流网WN有两个特殊状态：起始状态Mi和终止状态Mo。Mi表示起始库所i拥有唯一的库所，而Mo表示终止库所o拥有唯一的库所。
3 担保业务工作流网建模
3.1 担保业务与Petri网的映射
将担保业务流程中的角色映射为工作流网中的库所节点；角色之间的交互是是通过担保事务进行交互的，因此，将担保事务映射为工作流中的变迁节点；在担保事务中的交互状态或信息映射为工作流中的标记。担保业务流程与工作流网的映射关系如表1所示。
利用表1的映射关系，就可以用工作流网来刻画担保业务流程。
如图1所示的工作流网模型就是一个具体的担保业务流程的过程模型。该流程主要描述了企业客户在申请担保过程中所涉及的信息处理、交互及存档等。基于担保业务流程与工作流网的映射关系，通过定义库所、变迁节点及其关联关系，模型能够有效地描述该流程中的业务环节，并反映它们之间的时序关系。
该模型中的库所节点对应于担保业务流程的各个功能单元，其具体的对应关系如表2所示。
表3则给出了工作流模型中的变迁节点与担保业务流程中所包含的事务之间的对应关系。
3.2 模型的化简分析与验证
Petri网不仅为系统建模提供了形式化的手段和方法，更重要的是，Petri网具有丰富的分析和验证手段，包括基于状态方程的代数分析方法、基于可达性的图分析方法以及基于化简、分解等的归纳分析方法等，能够对模型进行有效的分析和验证，从而为实际系统高效正确运行提供保障。具体地，基于本文构建的工作流网模型，我们可以对担保业务管理系统及其工作流进行如下的分析和验证工作：
1）模拟和仿真：基于Petri网的可达图，我们可以模拟和仿真系统运行，求解所有可达状态，从而对系统的动态特性和运行机理进行深入的了解和理解；
2）定性分析：可以测试所设计的工作流是否能够达到预期的目标或满足特定的性质，包括安全性、可达性、活性及合理性（soundness）等；
3）定量分析：可以引入随机分析等定量分析技术，对担保业务管理系统工作流进行性能分析，包括平均服务时间、资源利用率等，为优化、调度、评价系统提供依据。
下面，我们以图1所示的工作流网为例，利用Petri网的化简分析技术，分析该模型的合理性性质，以表明模型分析和验证的有效性。事实上，合理性是工作流的重要性质之一，合理性保证了对于任何工作流实例，在没有异常的情况下，处理过程都能终止。W.M.P. van der Aalst[7]证明了工作流网满足合理性的充分必要条件是其扩展网（EWN）是活的和有界的，从而将合理性问题转化为Petri网动态性质的分析和验证。但性质判定方法可能会受到状态空间爆炸的约束，因此，很多学者研究了基于结构的分析方法，其中化简技术是最为常用的一种。在文献[8]中，就讨论了如何基于化简技术对工作流网进行合理性分析，文中提出了若干保持合理性的化简规则，并指出，如果一个自由选择扩展工作流网基于这些规则能将其化简为只包含一个库所和一个变迁的闭环网，则该工作流网是满足合理性的。
对于图1所示的工作流网，很容易验证其扩展网是自由选择网，因此可以利用文献[8]的化简方法，需要用到的化简规则包括如下的三条：
化简规则1：如果自由选择扩展工作流网EWN中输入输出弧都唯一的库所P的输入变迁ti与输出变迁to不是同一个变迁，P的输出变迁to的输出库所不为空且只有唯一的输入库所P，则库所P的输入输出变迁可以被融合成同一个变迁t（从而P被化简掉），t的输入输出库所分别是ti与t。的输入库所与输出库所的并，见图2(a)。
化简规则2：如果自由选择扩展工作流EWN网中输入输出弧都唯一的变迁t的输入库所Pi与输出库所Po不是同一个库所，t的输入库所Pi的输入变迁不为空且只有唯一的输出变迁t，则变迁t的输入输出库所可以被融合为同一个库所P(从而t被化简掉)，P的输入输出变迁分别是Pi与Po输入变迁与输出变迁的并，见图2(b)。
化简规则3：如果自由选择扩展工作流网中变迁t1，t2有相同的输入输出库所，则可以将t1，t2融合成一个变迁t，见图2(c)。
为了应用上述化简规则，首先扩展工作流网WN得到其扩展网EWN，其中增加的变迁为to，具体的化简过程如下：
步骤1：连续应用规则1，逐次消去符合规则1的库所，并相应的合并符合规则1的变迁，得到化简后的工作流网EWN1，见图3(a)所示；
步骤2：应用规则2，消去变迁t(3)，并合并库所o与p(2)，得到化简后的工作流网EWN2，见图3(b)所示；
步骤3：应用规则1，消去库所p(1)，合并变迁t(1)与t(2)，得到化简后的工作流EWN3，再图3(c)所示；
步骤4：应用规则2，消去变迁t1，合并库所o与i，最终化简为只含一个库所和一个变迁的闭环网EWN4，见图3(d)所示。
通过上述化简过程，我们将WN化简为只含一个库所和变迁的EWN4，说明该工作流网是满足合理性的。
4 结论
基于工作流网模型，本文给出了担保业务管理系统工作流的Petri网建模方法，构建了相应的形式化模型。利用该模型可以对担保业务管理系统工作流进行分析与验证。
本文的工作一方面为担保业务管理系统工作流定义了形式化模型，提供了理论分析与验证方法，从而为担保业务管理系统工作流的应用提供了理论支持，另一方面，也拓宽了Petri网模型及其理论的应用领域，相应地，新的领域和应用也必将出现新的理论课题和挑战，这也为Petri网理论的深入研究提出了要求，有助于丰富和发展Petri网基础理论。
参考文献：
[1] 袁崇义.Petri网原理[M].北京:电子工业出版社,1997.
[2] 吴哲辉.Petri网行为描述、性质分析与系统模拟[D].山东科技大学,2002.
[3] Der Aalst W M P, Hee K. 工作流管理一模型、方法和系统[M].王建民,闻立杰,译.北京:清华大学出版社,2004.
[4] 李建强,范玉顺.基于Petri网化简方法的工作流模型验证[J].信息与控制,2001,30(6):492-497.