工作流过程建模中验证技术的研究_图文

1、技 术 创 新中 文 核心 期 刊 微 计算 机 信 息 (管 控 一体 化 2008年 第 24卷 第 1-3期36元 年 邮局订阅号 6现场总线技术应用 例软 件 时 空1引言工作流 (workflow 是一类能够完全或者部分自动执行的经营 过程 , 它根据一系列过程规则 、 文档 、 信息和任务 , 能够在不同的 执行者之间进行传递与执行 。 在各种工作流相关技术中 , 工作 流的有效建模是开发健壮的、 合理的大型工作流系统的关键。 因 此工作流模型验证是工作流管理的一个重要组成部分。2过程 验证 研 究现 状工作流 过程定义中出现的错误可 以分为语法错 、 结构错和 语义错。 相应地有

2、语法验证、 结构验证和语义验证。 语法验证检 查过程 定义是否符合特定描述 语言的语法 ; 结构验证检查过程 定义是 否会导致错误执行 ; 而语义验证是 保证过程定义与实际 业务过程的目标一致性 。一 般可 识别 的验 证问 题主 要有 :(1初 始化 问题 (2 结 束问 题 (3 死 锁问题 (4 活 锁问 题 (5 迹 等价 问题 (6 安 全性 问题 (7 有 界 性问题。2.1形式化验证在工作 流建模研究中 ,Petri 网是 比较突出的具 有形式化基 础的工具 之一 , 利 于完成 过程验证 。 文献 的作者提 出了用 Petri 网 进行工 作流建模 的工 作流网 , 通过定 义

3、 1、 定义 2和定 理 1将 工作流模型的正确性归 纳为工作流网的合理性 , 并提出 了一种基于 Petri 网的图形化简方法辅助模型验证 。定义 1:Petri 网模型 W=(P,T ,F,i 是工 作流网络 , 当且仅 当 :(1 W 中存在两个特殊的库所 :库所是输入库所 , *i=, 库所 o 是输出 库所 , o*=; (2 如果在 W 中库所 o 和 i 之间增加一个变迁 i (即 i *=i, 且 t *=o , 则得到的 W 是一个强连通的 Petri 网 。 定 义 2:一个 工作流 网络 W=(P,T ,F 是合理的 , 当 且仅当 :(1 对于初始标志 Mi(库所 i

4、包含一个托肯的标志 可达的每一个 标 志 M , 存在一个启动顺序 , 使 得标志 M 可达标志 Mo , 即; (2标志 Mo(库所 o 包 含一个 托肯 的 标志 是从初始标 志可达的 , 则 M o 是唯一满足 库所至少包含 一 个 托 肯的 标 志 , 即; (3 在 (W,Mi 中不存在死的转移 , 即。 定理 1:工作流网络是合理的 , 当且仅当该网系统 (W,Mi 是 活的并且是有界的 。定义 1、 定义 2和定理 1成为基 于 P etri 网的过程合理性 验 证的 重要理论基础。通常 , 验证所采取的 办法是根据过程模 型 的 特点 , 选取便于 验证的几种 特性 (如安 全

5、性、 死锁等 , 然后 根 据性质间的因果关系导出合理性 。 目前的一 些验证研 究成果如 表 1所示 。表 1合理性验证基于 Petr i 网的形式 化验证优点在于 :(1合 理性定义清晰 ; (2验证方法具有良好的形式化基 础 ; (3 可验证的问题包括初 始 化 、 结束 、 死锁 、 活锁 、 安全性和有界性问题 。但是该方法 在实际应用中仍有一些 缺点 ( 有 些性质 (如 可 达性 、 覆盖性 等 的 验证需要构 造可达树或 可达图 , 在对大型 模 型进行 操作时可能造成状态空 间爆炸 ; ( 有些推导关系具有 条工 作 流 过 程 建 模 中 验 证 技 术 的 研 究Re s

6、ea rch o f Ve rifica tio n Tech niqu e s in Wo rkflo w Pro cess Mo d elin g(南昌大学 喻斌 武 友新YU BI N WU YOUXIN摘要 :工作 流过 程模 型的 验 证是 确保 工作 流系 统能 够正 确执 行的 至关 重要 的 一环 。对 近年 来 国内 外研 究 人员 在过 程 验证 方 面 的研 究和 成果 进行 了论 述 , 分 析说 明了 形式 化验 证 、 图 归 约法 等几 种 主流 方法 的 优缺 点 ; 结 合 工作 流 未来 的发 展 趋势 , 预 测 了过 程验 证下 一步 的研 究方 向 。

7、关键词 :过程验证 ; 佩特里网 ; 合理性 ; 归约 ; 关联矩阵 中图分类号 :TP311文献标识码 :AAbstra ct:Theverificatio n of wo rkflo w process model is o ne of the most important step to ensure that the workflow system can be exe-cuted correctly. Some research of process v erification in last years is presented in the issue , and the adv

8、antag e and disadvantage ofsome main methods are analyzed, such as formal verification and graph reduction. Then it predicts the research content of process verification in future according to the development of w orkflow.Key wor ds:Pr ocess Ver if ication, P etr i net, soundne ss, r eduction, Assoc

9、iation Ma tr ix文章编号 :1008-0570(200801-3-0220-03喻 斌 硕士基金 项目 国家 “ 63” 计 划软件 基金资助 重大项 目“ 基于 L x 的业务基础组件平台的研究与应用” (Z 0/:82-94200:12:8inu 2004AA12080220-邮局订阅号 636元 年 技 术 创 新软 件 时 空 L 技术应用 例 您的 论 文 得到 两 院院 士 关注件限制 , 这对更灵活的高级 Petri 网的使用造成了一定限制。2.2图归约法Wasim Sadiq 等 人提出了一种基于图 形归约的方 法进行工 作流过程验证 。 但这种方法只对工作流模型

10、结构中存在的特殊 问题 (与连接或同步的输入存在互斥的或分支及或连接的输入 中有属于同一个与分支的输出 进行了分析与验证 , 且这种方法 不适用于存在循环结构的工作流模型。 文献中对原归约规则进 行了修 正 , 解决了 其无法验证正确的嵌套结 构的问题 。 其归约 过程采用以下五种规则 :(1 顺序 (sequentia1归约规则如果和当前节点相连的弧数少于或等于 1, 则从图中删去 当前 节点 ; 如果当 前节点仅 有一条 输入弧和 一条输 出弧 , 且当 前节点 的前驱节点与后继节点 不是同一个节点 , 则将其输入弧 指向其后继节点 , 同时从图中删除该节点 。(2 循环 (iterati

11、ve归约规则若某节点是 Repeat /Until 型或 While /Do型 , 则递归调用归 约算法归约掉循环体中的活动及弧 。(3 邻接 (adjacent归约规则假 设当前 节点 为分支 型节点 (S plit, 若当 前节点 的后 继节 点 不是其前驱 节点 , 则将输 出弧转 移到其前 驱节点 上 , 同时删 除 当前节点 ; 如果当 前节点为 结合型节 点 (Join , 若当前 节点的 前驱 节点不是其后继节点 , 则 将其输入弧指向其后继 节点 , 同 时删除当前节点 。(4 闭合 (closed归约规 则一个闭 合结构包含两个具有相同 逻辑类型的节点 , 一个节 点为 Sp

12、lit 型 , 另一个 为 Join 型 , 从 S plit 型节点到 Join 型节点有 多条弧连接 。 应删除所有多余的弧 , 只保留一条弧 。 一个语法正 确的图只有当邻接结构被削减以后才会出现闭合结构 。(5 重叠 (overlapped 归约规则重叠结 构为第一层每个与分支 (And-Split 节 点都与第二层 每个异或结合 (Xor-Join 节点相 连 , 第二层每 个节点都与第三层 的 与结合 (And-Join 节 点相连 , 除了这 些弧 之外第 二层节 点没 有其它 相关联的弧。归约时第 二层的所有多余节点均被 删除 , 只留下一个节点。图归约法的优点在于 :(1能够

13、有效地缩减过程模型的规模 ; (2 易于理解 , 便于操作 。但图归 约法也有一个很大的缺点 , 就是对极 少数正确的过 程模 型不能进行归约。如图 1所示的过程模型 , 虽然过程是正 确的 , 但利用归约规则却无法将其归约为空。图 1图归约法无法归约的过程模型2.3邻接矩阵法文献中 提出了一种基于邻接矩阵 的过程验证算法 , 将图论 知识应用于工作流模型的结构验证 。 定义 3给出了将有向图邻 接矩阵扩展为工作流邻接矩阵 Wf M x 的过 程 。定 义 3设 W=(,T 是 由工作 流网 转换来 的简 单图 , 它有 个活动 =, , , , 则 阶方阵 (=(X j 称为工 作流网 W

14、的工作流邻接矩阵 , 简记为 Wf -Matrix 。其中 ,经过 了上述扩展后 , 由一个工作流过程就 可以很容易地 构 造 相应的工作流邻接矩阵 , 然后就可以 采用图论中有向图领 域 的相关算法来进行工作流结构验证。其验证过程可以分为四个 步骤 进行 :(1 由 工作流过程构造工作流 邻接矩阵 ; (2根据工 作 流邻 接矩阵 , 通过检 查各种 S plit 节点和 Join 节 点匹配情况 来 判 断工作流过程结构 的合法性 ; (3 应用图论中 W arshall 算法 , 由 工作流邻接矩阵构造工 作流可达矩阵 ; (4 根 据工作流可 达 矩阵判断工作流过程结构的连通性 。邻接

15、矩阵法可以有效地 验证以下几个方面 :(1是否存在 唯 一的 开始活动和结束活动 ; (2 由开 始活动出发 是否只能到 达 唯一 的活动 , 以 及是否存在唯一的活 动到达结束 活动 ; (3各 种 Split 节点与 Join 节点的 配对情况 ; (4 是否存在无效活动 。但它 同样存在着 不足之处 :(1 适用于 简单有 向图 , 没有 考 虑 图中有循环结构的情况 ; (2 当模 型规模较大 时有可能产 生 状态空间爆炸 。2.4其他验证方法及比较除了上 面介绍的三种方法外 , 研究人员还 提出了一些其 它 的过程验证方法 。 如文献论述了基于状态空间的验证方法 , 但 目 前大 多

16、数工作流建模都是基于 活动而不是基于状态 的 , 所以 该 方法的应用存在很大的局限性 。 文献提出用过程逻辑的方法验 证 工作流 , 有效 地解决了 死锁的 问题 ; 但是 并未解决 工作流 过 程中的同步丢失问题 , 也没有论述如何验证有环工作流过程 (即 过程模型中带有循环路由 。下面 从验证过程是否包含循环 、 能否有效 解决死锁和同 步 丢 失、 运算的复 杂程度以 及验证 的完整性 等方面 , 归 纳了上 述 五 种验证方法的性质如表 2所 示。从表 2可以看出 , 当前的 工 作 流验证方 法在运 算的复杂 性和验 证的完整 性两方 面还无法 同时达到一个满意的水平。表 2各种工

17、作流验证方法的性质3进一 步研 究 方向以 上 我们 所 介绍 的 方法 都 是 基 于结 构 验 证方 面 的 。由 WMFC 工作流 过程元 模型可 以知道 , 一个完 整的过程 模型 应该 包括控制流 、 数据流和 资源三 个要素 , 只有 完整地 检查三维 元 信息共同 作用产 生的冲突 才能确 定一个过 程能否 真正正确 实现 其业务目标 。 所 以我们还要 对过程模型 进行语义验 证。 文 献 提出了一 种三维 的扩展 网 3DWF N , 并基于 该形 式 化 模型总结 出化简 规则以 进行语义 验证 。 与 语义验 证作用的:82-940/P C 200-atri :P n P

18、 a1a2an n P w i Petri 221-技 术 创 新中 文 核心 期 刊 微 计算 机 信 息 (管 控 一体 化 2008年 第 24卷 第 1-3期36元 年 邮局订阅号 6现场总线技术应用 例软 件 时 空重要 性相比 , 目前的 研究人 员在语义 验证方 面所进行 的研究 却 存在着很大 的空白 , 所以今 后过程 验证的 重点将会 偏向于 语 义验证 。另一 方面 , 随着 工作流 技术应用 的越来 越广泛 , 对 于工作 流技术 的要求也越来越高 。 分 布式 、 异构性 、 高效柔性 、 跨领域 协同 工作、 智能化 是现代工 作流技 术的发展 趋势 , 这就 意味

19、着 过程模型也将向着灵活、 动态、 自适应等方向发展。 而我们目前 的大多 数过程验证都属于静态验 证 , 无法满 足工作流技术的发 展要求 。 如何保证动态柔性模型的正确性也将是今后过程验证 研究的一个热点 。4结束 语工作流 模型是工作流应用的生命 线 , 模型的 可用性直接受 模型质 量的影响 , 因此对于如何确保模型质 量的研究一直是工 作流工作者十分关注的问题 。 本文对近年来国内外在工作流过 程验证 方面的研究及其成果进 行了比较说明 , 分析了几种主流 方法的 优缺点 ; 最后 , 对工作流 过程验证的发展趋势作了 预测 , 指出了其进一步的研究方向。本文作者创新点 :对目前主流

20、的几种工作流过程验证方法进 行了比较说 明 , 分析了各 种方法 在应用中 的优缺 点 , 并结合 工作流系统的发展趋势指出工作流下一步的研究方向。 参考文献 :inconceptual w orkf low specif ications.Data and Knowledge Engineer-ing.1998,24(3:239-2563WM P van der Aslst.The Application of Petri Nets to Wor kf low Management.The Journal of Circuits,Systems and Computers.1998.8(1

21、:21-664程刚 . 一种工作流模型结构验证的有效 方法 Z. 大连 :大连理工 大学 ,2005.5ZHAO Lei,QIAN Leqiu,ZHAO Wenyun.S tate -space based veri-f ication of w orkf low modelJ.Computer Engineering &Application, 2004,40(10:220-222.6HENRY H B,ZHAO L.Process logic f or verifying the corr ectness of business process models A.Proceedings o

22、f the 2004I nterna-tional Conf erence on Information S ystems(2004I CIS C.Washing-ton,D.C.,USA,2004.91-100.7周建涛 , 史美林 , 叶新铭 . 一种 基于 Petri 网 化简的工作 流过程 语义验证方法 J.软件学报 ,2005,16(7 :1242-1251.8李伟 , 李青 . 基于 J2EE 的 工作流管 理系统 框架研究 与实现 J微计算机信息 ,2004,20(8 :97-99.作者 简介 :喻 斌 (1984-, 男 (汉族 , 江西 临川人 , 硕士 , 主要 研究方 向

23、 :数据 库 、 电子政 务 ; 武友新 (1963- 男 (汉族 , 江西南 昌人 , 教 授 , 硕导。Biogr a phy:BinY u (1982-, Male (theHan Natio nality, Born in Linchuan City of Jiangxi Province, Master o f Science ,Specialin:Database Dev elopment, Electronic Government Affair ; Y ouxinWu(1963-,Male (theHan N ationality,Born in Nanchang City o

24、f Jiangxi Pro vince ,Professor and M entor o f postg raduate stu-(33江西南昌 南昌大学信息工程学院 喻斌 武友新 (If I f f N U y,Na nchang, 330029, C hinaYu Bin Wu YouXin通 讯地址 :(330096江西省 南昌 市高 新大街 火炬大 道 681号 思创数码科技股份有限公司软件部 喻斌(上接第 314页 4.4收敛性依据式 (9 计算收敛函数 。 图 4给 出了恢复图像的均方差 函数随迭代次数的变化曲线 。图 4用联合变换算法计算相位函数时的收效结果5小 结与 本 文作 者创 新 点本文综合多种 随机相位加密 技术 , 找到不同 加密方法的 优点 和缺点 , 提出在联 合变换相关器上 , 进行纯相位加密的改进 方 法 。 不仅进行了计算机模拟算法实验 , 同时给出了实际的光学再 现图像 。 证明了 在联合变 换相关器 上的纯相位 加密方法 的正确 性和可行性。 参考文献 :1国承 山 , 王