（计算机科学与技术专业论文）工作流模型性能分析与形式化验证：一种基于扩展petri网的方法.pdf

国防科学技术大学研究生院工学硕士学位论文 摘要 模型的性能分析以及过程验证是工作流系统研究和应用的重要内容。根据8 6 3 项目“面向金融领域的分布式工作流关键技术及应用框架”对于工作流仿真和验 证的需求，针对p e t r i 网在复杂工作流建模中模型规模庞大、描述功能有限以及缺 乏层次化特性等不足，本文提出了一种基于扩展层次有色p e t r i 网( e h c p n ) 的工 作流过程模型仿真与验证方法。e h c p n 模型包含p e t r i 网的所有特性，并在p e t r i 网基础上增加了层次化结构特征，简化了模型的结构，并引入面向对象的建模思 想，提高了模型的可读性，适合工作流的建模与分析。 本文主要工作在于工作流模型的建模、仿真与验证。首先，对e h c p n 进行形 式化定义，给出将工作流过程模型转换成工作流e h c p n 模型的转换规则。然后， 基于e h c p n 模型，设计并实现了一个支持工作流建模、仿真和验证的集成环境： w f 删s e 。在w f - p t m s e 的验证部件中，提出了状态组构造算法，该算法能 够较为高效地构造验证所需的状态空间，从而完成对工作流e h c p n 模型的验证。 最后，通过多个具体的工作流过程模型案例，在、v f p t m s e 环境中创建对应的 e h c p n 模型，对该模型进行仿真分析以及验证分析，并分别给出仿真与验证相应 的实验数据和分析结果。 仿真与验证的结果表明，e h c p n 模型良好的数学定义和强大的描述能力能够 正确有效地表达工作流的结构特性；基于e h c p n 模型的w f - p t m s e 集成环境能 够支持工作流的建模、仿真和验证的全过程；状态组构造算法能够高效地构造 e h c p n 模型的状态空间，提高工作流e h c p n 模型的验证效率。 主题词：工作流p e t r i 网过程模型仿真模型检验 第i 页 国防科学技术大学研究生院工学硕士学位论文 a b s t r a c t p e r f o r m a n c ea n a l y s i sa n dp r o c e s sv e r i f i c a t i o no fw o r k f l o wm o d e li so n eo ft h e m o s ti m p o r t a n ta s p e c t so nt h er e s e a r c ha n d a p p l i c a t i o no f w o r k f l o ws y s t e m a c c o r d i n g t op e t r in e t ss h o r t a g et h a tm o d e l i n gs c a l ee n o r m o u s l y ，l i m i t a t i o no fi t s d e s c r i p t i o n f u n c t i o na n dn oc h a r a c t e r i s t i co fh i b e r a r c h y , t h i sd i s s e r t a t i o np r o p o s e sa ne x t e n d e d h i e r a r c h i c a lc o l o r e dp e t r in e t ( e h c p n ) a p p r o a c ht os i m u l a t ea n dv e r i f yt h ep r o c e s so f w o r k f l o wm o d e l ，w h i c hr e m e d ys h o r t a g eo f p e t r in e t e h c p nm o d e li so b j e c t - o r i e n t e d ， w h i c hi sc o m p r e h e n s i v ea n di m p r o v ee f f i c i e n c yo fm o d e l i n ga n da n a l y s i so fw o r k f l o w m o d e l t h i sd i s s e r t a t i o np l a c e se m p h a s i so nt h em o d e l i n g , s i m u l a t i n ga n dv e r i f i c a t i o no f w o r k _ f l o wm o d e l f i r s t l y ，w ef o r m a l i z ee h c p nm o d e l ，a n dg i v ear u l ew h i c ht r a n s f o r m f r o mw o r k f l o wm e t a - m o d e lt ow o r k f l o we h c p nm o d e l b a s e do nw o r k f l o we h c p n m o d e l ，w ed e s i g na n di m p l e m e n tas u i t eo f t o o l s ，w f 嗍s e ，w h i c hm o d e l ，s i m u l a t e a n dv e r i f yw o r k f l o w o nt h ep a r to fv e r i f i c a t i o n , w ep r o p o s eas t a t eg r o u pc o n s t r u c t i o n a l g o r i t h m ，w h i c hc a n c o n s t r u c ts t a t es p a c e sn e e d e db yv e r i f i c a t i o nq u i t ee f f i c i e n t l y a t l a s t , w ec r e a t ec o r r e s p o n d i n ge h c p nm o d e li nw f p ，n “s et h r o u g hs o m ec a s e so f w e t k f l o wp r o c e s sm o d e l ，w h i c hi ss i m u l a t e da n dv e r i f i e d , a n dg i v et h ed a t aa n dr e s u l t s o f s i m u l a t i n ga n dv e r i f i c a t i o ns e p a r a t e l y t h er e s u l t so fs i m u l a t i n ga n dv e r i f i c a t i o ns h o wt h a tf a v o r a b l em a t h e m a t i c a l d e f i n i t i o na n d p o w e r f u ld e s c r i p t i o nc a p a b i n t y o fe h c p nm o d e lc a ne x p r e s s w o r k f l o w ss t r u c t u r a lc h a r a c t e r i s t i c sc o r r e c t l y , e h c p n b a s e d 、f - p t m s ec a l ls u p p o r t a l lt h ep r o c e s so fm o d e l i n g ，s i m u l a t i n ga n dv e r i 句h a gw o r k f l o w , a n ds t a t ec l a s s c o n s t r u c t i o na l g o r i t h mc a nc o n s t r u c tt h es t a t es p a c e so fw o r k f l o we h c p nm o d e l e f f i c i e n t l y ，a n di m p r o v ee f f i c i e n c yo f w o r k f l o we h c p n m o d e lv e r i f i c a t i o n k e yw o r d s ： w o r k f l o wp e t r in e t m o d e lc h e c k i n g s i m u l a t e 第i i 页 国防科学技术大学研究生院工学硕士学位论文 表目录 表3 1 工作流过程模型元素及其图形表示 表4 1 工作流活性和安全性的c t l 常用公式型 表5 1 商场收银统计数据 2 6 4 7 5 2 表5 2 模型状态空间与e h c p n 模型标识集的对应关系。5 3 表5 3 模型的时态逻辑属性检验结果 第1 页 国防科学技术大学研究生院工学硕士学位论文 图目 图2 i 工作流管理系统的特征 图2 2 工作流模型的组成结构 图2 3 模型检验上下文结构图 图2 4c t l 表达式图示 图3 1p e t d 网状态变换图示2 2 图3 2 传感器信息处理模型2 3 图3 3e h c p n 的简单图示2 4 图3 4 输入端口 图3 5 输出端口。 图3 6 库所。 图3 7 变迁。 图3 8 可控变迁。 图3 9 顺序模式的转换。 图3 1 0 并行分支模式的转换 图3 1 1 同步模式的转换 图3 1 2 排它分支模式的转换 图3 1 3 简单合并模式的转换二 图3 1 4 多路分支模式的转换 图3 1 5 多路合并模式的转换 图3 1 6 循环模式的转换 图3 1 7e h c p n 模型的嵌套模式 图3 1 8e h c p n 模型的嵌套模式的内部结构图示 图4 1w f - p t m s e 仿真验证环境的逻辑结构。 图4 2w f - p t m s e 库所、变迁、端口和弧的类关系图 图4 3 类库中类的结构 图4 4w f p 厂r m s e 建模环境主界面 图4 5 仿真器一个周期内的运行流程 图4 6w f - p t m s e 仿真环境主界面。 图4 7 变迁多实例图示 2 6 2 7 2 7 2 7 。2 7 。2 8 。2 8 。2 9 。2 9 3 0 3 0 。3l 。3l 31 3 2 3 4 3 5 3 7 4 0 4 l 图4 8 模型检验器结构图。 图5 1 收银管理系统的收银过程模型 图5 2 收银台工作的e h c p n 模型 4 2 4 4 4 6 。5 0 5 0 第1 v 页 n ” 国防科学技术大学研究生院工学硕士学位论文 图5 3 赠品台工作的e h c p n 模型 图5 4 付款工作的e h c p n 模型 图5 5 信用证到单子系统流程 ：i ：! 5 6 图5 6 信用证到单子系统的e h c p n 模型5 6 图5 7 委托运输业务流程 图5 8 委托运输业务的e h c p n 模型 图5 9 信访流程 图5 1 0 信访过程的e h c p n 模型 5 7 ! i 7 第v 页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得的研 究成果尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已 经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它教育机构的学 位或证书而使用过的材料与我一同工作的同志对本研究所做的任何贡献均已在论文 中作了明确的说明并表示谢意 学位论文题目：乏聋盗攫型选钝泌曼型盎坐验近! 二赶墓i 芷鏖丝! 亟妇右泼 学位论文作者签名：金签日期：细占年月，弘日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留，使用学位论文的规定本人授权国 防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子文档，允 许论文被查阕和借阕；可以将学位论文的全部或部分内容编入有关数据库进行检索， 。可以采用影印，缩印或扫描等复制手段保存。汇编学位论文 ( 保密学位论文在解密后适用本授权书) 学位论文题甘：暑b 罐翌挫位尘趱型蠡焦墨盆迂匕孟墓i 垃蜃至鲢 i 遛的南渡 学位论文作者签名：金么日期触年弓月，乒日 作者指导教师擞：二舡日期：加6 年岁月，中日 国防科学技术大学研究生院工学硕士学位论文 第一章引言 1 1 课题背景 工作流技术是近年来在计算机领域中发展最为迅速的几项新技术之一，已经 广泛应用于办公自动化、文件管理、目录管理、群件应用、b p r ( b u s i n e s s p r o c e s s r e e n g i n e e r i n g ) 等领域1 5 】。这些领域在处理过程中的共同点是侧重处理一些具有固 定程序的常规活动，工作可划分成任务，并指派执行者，且在执行中遵守相应规 则。起初，过程完全由人操作物理对象来完成。随着信息技术的产生和发展，过 程被逐渐的部分或全部计算机化。现在，工作流技术正因计算机和网络技术的进 步而得到前所未有的发展。 工作流是一类能够完全或者部分自动执行的业务过程，它根据一系列过程规 则使得文档、信息或任务能够在不同的执行者之间传递或执行，以达到确定的业 务目标。工作流技术是实现业务过程的建模、仿真分析、优化、管理与集成，从 而最终实现业务过程自动化的核心技术【1 】。利用工作流技术进行建模和分析，可以 规范业务过程，发现其中不合理的环节，进而对业务过程进行优化重组。 工作流模型是将现实世界中的业务过程抽象出来，并用一种形式化的、计算 机可处理的方式来表示，这种形式化结果成为工作流模型 6 0 1 。工作流过程建模作 为一项支持企业过程集成与优化的技术，是对企业系统中与企业过程相关的特性 加以抽象表达并动态仿真企业内部各种行为活动的一种方法，是企业过程集成成 功的前提同时工作流模型是工作流管理系统的基础，它决定了系统的行为和功 能特性。良好的工作流模型应能够严格规范工作流的运行规则，从而使工作流执 行程序能在运行时解释工作流模型，正确调度和分配任务。随着网络技术的进一 步发展，企业中和企业问的业务过程变得越来越复杂，并且将向具有灵活性、自 适应性、规模可扩充性以及互操作性等先进特性的方向发展。由此，对这些过程 进行建模的复杂性势必相应提高虽然工作流建模技术在不断的发展，但是需求 的不断增加需要工作流建模技术更进一步的提高因此对工作流模型的合理性、 可用性和正确性的分析和验证是很有现实意义的 近年来，工作流模型仿真的分析与研究是工作流研究的一个热点工作流模 型仿真分析是支持业务过程重组的一种行之有效的分析手段业务过程重组是对 企业的经营过程进行重新思考与再设计，以追求企业性能的突破性提高。业务过 程重组的实旄需要通过先进的过程建模和分析手段来描述、分析和评价业务过程， 发现其中的问题并对其进行优化工作流模型仿真是指用仿真引擎模拟活动的执 行，自动推进工作流实例，其目的是定量的分析业务过程的各项性能指标，例如 第l 页 国防科学技术大学研究生院工学硕士学位论文 过程的运行时间、运行成本和资源的利用率等，判断经营过程中是否存在瓶颈和 死锁因素，经营过程的性能是否良好t 6 0 l 。仿真结果可以作为经业务过程的评价、 过程改进方案的可行性和有效性验证的依据，也是企业进行决策的参考。 般来说，工作流模型仿真的主要作用体现在两个方面【l 】：一方面，仿真模拟 过程模型的执行，以便及早的发现模型设计中的问题并进行相应的修改；另一方 面，对新创建的过程模型在未实施的情况下，借助仿真功能来分析评价其运行结 果，以辅助选择最优的过程模型。 工作流过程模型形式化验证是复杂工作流过程建模中需要的重要功能之一， 这一点不仅得到学术界的重视，而且也得到了工业界的重视。工作流过程越复杂， 验证需求越迫切，具体表现【5 】如：隐含错误的大规模过程投入操作，一旦发现失 败，修改周期长、代价大；柔性建模方法可以满足动态修改过程定义的要求， 却并不保证修改后流程的正确性；跨企业过程之间的互操作将带来更易出错的 因素，并且错误的检测也相对困难。工作流过程模型形式化验证的目的就是试图 使开发者在建模初期高效的发现并改正过程模型中的结构错误、语法错误以及语 义错误，构造出高可靠性的系统。形式化验证的方法种类很多，对于工作流过程 模型的验证，i i 前较多采用模型检验的方法，后文中将对模型检验理论做进一步 的介绍。 综上所述，工作流的建模、仿真及验证是工作流建模时期十分重要的三项工 作。这三项工作逻辑关联紧密：理想的工作流模型能够清楚的定义任意情况下的 工作流，能够适应用户在建模过程中所提出的各种要求；而仿真及验证的方法和 工具的选定，仿真的内容和性能指标的确定，验证可检验错误的确定将反映出建 模的正误和模型的优劣；在一定意义上，验证可以看作仿真的一部分，验证确保 了模型的正确型，从而使得仿真顺利的进行，而仿真又从模型的运行角度考虑模 型的优劣问题，为工作流系统的开发工作起到良好的指导作用。 1 2 工作流性能分析与验证方法概述 目前，对工作流进行性能分析与验证主要包括两种方法【5 】：形式化验证方法和 模拟方法 形式化验证方法使用数学方法形式化的证明设计实现部分或全部满足系统描 述要求目前形式化验证方法种类较多。模型检验1 2 l ( m o d e lc h e c k i n g ) 是一种检 测设计是否具有所需属性的方法；等价性检查1 2 1 ( e q u i v a l e n c ec h e c k i n g ) 用于比较 设计的两种实现是否一致，该方法又可分为组合等价性检查( c o m b i n a t i o n a l e q u i v a l e n c ec h e c k i n g ) 和时序等价性检查( s e q u e n t i a le q u i v a l e n c ec h e c k i n g ) 其 它的方法还包括定理证明 5 1 ( t h e o r e mp r o v i n g ) 和符号轨迹求解【5 】( s y m b o l i c 第2 页 国防科学技术大学研究生院工学硕士学位论文 t r a j e c t o r ye v a l u a t i o n ，s t e ) 等。在形式化验证方法中，通常使用k r i p k e 结构【2 】 来描述反应式系统，描述这种系统的状态变化。k r i p k e 结构m 被定义为一个三元 组m _ s ，s o ，r ，其中s 是一个有限状态集合，s o 是初始状态集合，r c s s 是 转移关系。2 2 1 节将对k r i p k e 结构做详细介绍。下面简单介绍三种主要的验证和 分析方法。 1 模型检验 模型检验用于检测某个具有有限状态集合的系统是否有其描述所规定的属性 【8 1 【9 1 。描述通常用时态逻辑表示，例如计算树时态逻辑【9 】( c o m p u t a t i o nt r e el o g i c ， c t l ) 和线性时态逻辑【l 们( l i n e a rt e m p o r a ll o g i c ，l t l ) ，而系统被建模为k r i p k e 结构。早期的模型检验方法是显式状态搜索方法【“】，该方法的缺点是状态爆炸问 题。m c m i l l a n 掣1 2 1 提出了基于化简有序二分决策卧1 3 1 ( r e d u c e do r d e r e db i n a r y d e c i s i o nd i a g r a m , r o b d d ) 的隐式状态搜索检测方法，称为符号模型检验。 2 定理证明 在定理证明中，系统及其需满足的属性都用数理逻辑的形式化语言描述，一 个形式化描述的系统包括一组公理和演绎规则，从系统的公理找到对属性的证明 的过程就被称为定理证明【l ”。与模型检验不同，定理证明能在无限状态空间上进 行推理。 3 模拟验证方法 ， 该方法主要通过模拟工作流过程模型，实现对工作流过程模型在执行过程的 行为进行分析，主要用于性能评价和流程评估。 1 3 研究现状 1 。3 1 工作流形式化验证的研究现状 工作流技术作为现今软件领域的研究热点，保证其正确性是工作流发展所需 解决的重要问题之一由于工作流模型的复杂性【4 l 】，目前还没有有效的算法可以 对工作流模型的正确性进行分析文献【6 】总结了需要验证的一些特性，例如，无 死锁( d e a d l o c kf r e e n e s s ) 、无乏同步( 1 a c k - o f - s y n c h r o n i z a t i o nf r e e n e s s ) 、类活性 ( q u a s i l i v e n e s s ) 、活性0 i v e n e s s ) 、有界性( b o u n d e d n e s s ) 、起始状态( h o m es t a t e ) 等 工作流过程模型中经常需要验证的是活性和安全性以及工作流实际需求等属性。 工作流模型验证方法有基于图形理论的方法、基于线形代数的方法和基于状态的 方法等。文献 7 e e 提出一种基于无环有向图( d a g ) 的可视化验证方式和算法，并 给出和使用了一系列化简规则来识别出过程模型中的结构冲突，同时也对化简过 程的正确性和复杂性进行了探讨。文献【4 2 】提出一种基于图形化简的方法进行工作 第3 页 国防科学技术大学研究生院工学硕士学位论文 流模型验证，并归纳了几种化简规则，但这种方法只对工作流模型结构中存在的 特殊问题( “与连接”“或同步”的输入存在互斥的“或分支”及“或连接”的输 入中有属于同一个与分支的输出) 进行了分析与验证，而且这种方法不适用于存在 循环结构的工作流模型。由于p e t r i 网严格的数学基础和图形化的规范语义，对于 工作流的建模与分析研究人员来讲具有很大的诱惑力，文献 2 】中提出了用p e t f i 网 进行工作流建模的工作流网，将工作流模型的正确性归纳为工作流网的完整性， 并在文献【4 3 冲提出了一种基于p e t r i 网的图形化简方法辅助模型验证，但是其提 出的化简步骤由于不具有完备性而不能完全验证工作流模型的正确性。文献 8 】提 出了一种基于p e t r i 网化简规则的工作流过程模型验证方法，并证明了所提规则的 完备性和多项式时间复杂性。此外，文献【4 4 】中提出了一种基于仿真的模型验证方 法，但它缺乏理论上的严格证明，而且当发现系统中确实存在冲突或死锁时，并 不能确定具体是在什么部分出现的问题( 只是给出了一些辅助的检测数据) 。 总的来说，常用的验证思想包括合理化验证理论和化简验证等【5 】。合理化验证 基于p e t r i 网技术，根据过程模型的特点，选取便于验证的几种特性( 如安全性、 死锁等) ，然后根据性质问的因果关系导出合理性。w o f l a n 是一种基于合理性验 证理论的工具，其主要功能有语法检查、结构错误检钡4 ，如a n d 或o r 是否配对 等；动态特征检测，如非安全的库所、死变迁等；以及库所和变迁不变量的检查 等。 合理化验证的定义清晰，验证方法具有良好的形式化基础，可验证的问题包 括初始化、结束、死锁、安全性和有界性问题。但是在实际应用中该方法仍有很 多缺点，例如，有些性质( 如可达性，覆盖性等) 的验证需要构造可达图或可达 树，在对大型模型进行操作时可能造成状态空间爆炸。 化简技术的基本思想是在特性保持的原则下，将过程模型化简为适当规模， 以便检测各种冲突。从工作流过程描述模型来看，主要有基于工作流图和基于p e t r i 网的两类化简方法。基于工作流图的化简方法可检测过程中的死锁冲突。基于此 化简技术的工具有f l o w m a k e 5 3 】。基于p e t r i 网的化简技术可在特性保持的前提下， 将过程模型缩d , n 适当规模。这样，在分析系统时就可以面对较小的状态空间， 使很多基于p e t r i 网的分析方法成为更实用的技术。 化简验证技术的核心思想是缩减模型的规模，以便进行验证化简技术中总 结的规则集便于操作和实现工具自动化。 1 3 2 工作流性能分析的研究现状 由于业务流程建模是工作流描述的重要内容，模型的性能评价是工作流系统 研究和应用的主要理论基础和支撑技术，因此对模型的性能分析是工作流的一个 第4 页 国防科学技术大学研究生院工学硕士学位论文 重要研究内容。目前，工作流模型分析方面的研究取得了一定的成果。文献 2 】指 出了工作流模型分析的不同方式，并将工作流模型的分析分为三种类型： 确认( v a l i d a t i o n ) ：检查和测试工作流是否达到了预期的结果通常运用交 互模拟技术把一些模拟用例输入系统，观察是否达到预先所期望的功能。 验i 正( v e r i f i c a t i o n ) ：检验是否正确的建立了工作流模型。通常可以使用线 性代数理论和基于p e t r i 网的分析技术等。 性能分析( p e r f o r m a n c ea n a l y s i s ) ：通过处理时间、服务成本、资源利用率 等数据来评价业务过程满足需求的能力。通常可以使用模拟和马尔科夫链 方法 目前很多文献针对工作流某一方面的特性分析改进了工作流的性能，如文献【3 】 根据客户服务器工作流模型来对工作流的性能进行分析；文献【4 】根据具有时间限 制的工作流模型来对工作流的性能进行分析等。 然而事实上，相对于建模和执行来说，工作流仿真还是一个比较薄弱的环节， 尚处于以研究为主的状态，离商品化的距离还比较远。在缺乏仿真方法与仿真工 具支持的情况下，整个工作流系统是不完善的。因为人们难以预料所部署的工作 流过程将有可能出现怎样的结果。针对工作流进行仿真的难点主要在于【2 9 】：仿真 的性能指标难以确定，仿真的内容较为复杂等。近几年来，国内外在对业务流程 建模仿真研究的基础上，开始思考工作流仿真额【3 0 】问题，该研究主要侧重于两个 方面：一是工作流仿真性能指标，二是工作流仿真机制及体系结构。前者主要是 提出性能指标及其相关的分析方法，常用的指标有完成时间、活动成本和资源利 用率等，分析方法有时间( 成本) 关键路径、计划评审技术、a b c 成本分析法等 【3 1 】【翊。后者对于如何建立工作流仿真系统的探讨分为两种思路。 一种思路是结合已有的工作流建模工具和商业化的离散系统仿真分析工具， 通过模型映射，建立新的工作流仿真系统。例如，文献 3 3 1 中汉城大学工业设计系 开发的s n u f l o w 工作流管理系统包括四个模块：流程设计，工作流引擎，工作流 客户端和工作流监视器。为了增加仿真功能，他们开发了一个新的模块w f s i m ( w o r k f l o ws i m u l a t i o n ) 鉴于工作流模型和离散系统仿真模型在活动和事件概念 上的相似性，该模块可以完成从s j f l o w 过程定义语言( p d l ：p r o c e s sd e f i n e l a n g u a g e ) 到s i m a n 仿真语言的转换工作，这样就可以直接利用s i m a n 这个成 熟的商业仿真工具进行后续的工作当然在转换过程中，需要做一定的假设。文 献 3 4 】利用角色活动图( r a d ：r o l ea c t i v i t yd i a g r a m s ) 建立流程模型，通过三个 步骤完成到w i t n e s s 系统的模型映射：首先是基本映射，把r a d 基本信息转换 成w i t n e s s 可以理解的信息；其次由用户输入r a d 没有提供的必要的仿真信息 ( 如：运行时间和到达时间等) ；然后结合这两部分信息完成映射，自动生 第5 页 国防科学技术大学研究生院工学硕士学位论文 w i t n e a s s 仿真代码。文献 3 5 1 开发了支持金融部门业务过程建模和( 再) 设计 的语言、方法和软件工具t e s t e ds t u d i o 。主要思想之一就是用一种图形建模语言作 为不同分析工具的公用前端。建模包括行为模型和角色模型。利用已存在的仿真 和分析工具，建模者无需了解分析技术的细节，减轻了他们的负担。这种思路着 眼于利用已有的工具，满足项目需求，省时省力。 另一种思路是建立一个完全自主的工作流仿真系统，包括仿真模型和仿真引 擎，以及分析工具1 3 6 1 1 3 7 1 0 8 3 9 1 。例如，文献 3 6 】提出了基于功能网的工作流模型建 模和仿真工具，其功能网是在标准p e t r i 网基础上，综合了延时、着色和扩充特征， 以及冲突解决和其他一些功能特性。文献 3 8 1 1 4 0 提出了基于工作流的企业过程的 建模、仿真、使能系统的模型和体系结构，将工作流模型转化为集控p e t r i 网来实 现企业过程仿真，提供了仿真过程中时间和成本等性能参数的计算和分析方法。 这种思路利用自己的建模方式和仿真引擎，可以按实际需要来仿真业务流程，不 必为了迁就已有的软件功能而进行简化和折中。 目前有很多方法都可以用来进行工作流过程模型的定义和描述，如：w f m c 定 义语言、e p c m 一模型、p e t r i 网等。尽管各种工作流建模方法形式上不尽相同，但 它们都能提供对逻辑顺序结构，资源使用，路由控制信息等流程定义所必须的要 素的描述。p e t r i 网作为一种优良的形式化描述工具已被广泛的应用在工作流建模 与性能分析等各个方面。在上个世纪的最后二十年的时间里，传统的p e t r i 网已经 发展到有色p e t r i 网、时间p e t r i 网和混合p e t r i 网等高级p e t r i 网。高级p e t r i 网 的出现使含有数据和时间等重要因素的复杂过程的建模变得十分容易。许多研究 者利用p e t r i 网的分析技术提出了一些工作流的性能分析方法，并建立了工作流的 性能分析工具。比较传统而典型的有文献【2 3 】中基于随机p e t r i 网模型的性能参数 的分析方法和利用性能等价的约简方法分析工作流系统服务周期吞吐率以及系统 中平均任务数等的方法。文献【2 7 】通过建立扩展随机p e t r i 网模型，将工作流管理 联盟定义的工作流模型映射为广义随机工作流网络，利用广义随机p e t r i 网与马尔 可夫链的等价关系得到一种p e t r i 网与马尔可夫链理论相结合的工作流性能分析方 法。 1 4 问题提出与研究内容 随着工作流系统规模和复杂性的不断增大，系统出错的几率也随之增大。而 定义和模拟真实世界的工作流是一个非常复杂且容易出错的过程，工作流模型的 错误定义将导致工作流实现的错误，在系统运行之后再更正错误将造成巨大损失。 然而，目前有些工作流系统只提供非常基础的语法检查，很少提供整个流程正确 性的检查方法。其中的原因并不是因为系统的设计者没有认识到过程验证的重要 第6 页 国防科学技术大学研究生院工学硕士学位论文 性，而是因为这项工作从技术角度来看是非常困难的，这个问题引起了学术界和 工业界的高度重视。 工作流过程模型形式化验证的目的是试图在工作流建模初期准确的发现并改 正过程模型中包含的各类错误( 包括结构错误、语法错误以及语义错误等) ，从 而构造出高可靠性的系统。达到这一目标的方法之一就是使用形式化方法。形式 化方法是以数学为基础的用于对系统进行规格说明和验证的语言、技术和工具等 的总称【l 】。规格说明是对系统及其性质进行描述的过程。使用它可以精确的描述系 统的行为和性质。它是需求者和设计者、设计者和实现者、实现者和测试者之间 极其有用的沟通工具，是系统编码的补充文档。形式化验证的方法主要有模型检 验和定理证明两种，其中，模型检验是目前使用最广泛、被认为是最有效的。 在工作流过程模型的形式化验证中，主要关心两类正确性属性：安全性( s a f e t y p r o p e r t i e s ) 和活性( 1 i v e n e s sp r o p e a i e s ) 。文献 5 8 】给出了安全性和活性的形式化 定义。对于任意集合，9z 。表示所有有限和无限序列集合，即a 上的u 一序列。 对于任意一序列t = ( t 。，t l ，) ，和非负整数i ，j ，j i ，定义序列t ( i ) 和 t ( i 。j ) 为：t ( i ) = ( t “t l ，”，t 。) ，t ( i ，j ) = ( t 。，t 。，t ，) 。t ( i ) 是t 的前缀，它包 含前i + 1 个元素，t ( i ，j ) 是t 中第i + l 到j + l 之间的元素序列。一个属性是。的 一个子集 定义l ( 安全性( s a f e t yp r o p e r t i e s ) ) 属性c 为安全性，当且仅当所有t 。满 足下列条件： 若任意的i 0 ，存在h e 。，使得t ( i ) u e c ，则t c 。 由此定义可知，一个属性为安全性，当且仅当每个不满足该属性的活动都有 一个不满足该属性的有限前驱活动，反之，如果一个活动的有限前驱活动不满足 该属性，则该活动本身也不满足该属性。 定义2 ( 活性( s a f e t y p r o p e r t i e s ) ) 属性c 为活性，当且仅当集合 t ( i ) ：t c 是z 。 由此定义可知，一个属性为活性，当且仅当对于每个有限活动序列，至少包 含一个后继活动。 工作流的验证工作必须在合适的工作流模型中得以实施。目前，在众多的工 作流建模方法中，p e t r i 网是一种图形语言，可直观的反映并行、同步和共享等现 象，适合描述具有并行行为或操作的系统。p e 缸i 网的另一特点是具有精确的语义 和严格的数学基础，其理论结果十分丰富。p e t r i 网模型把系统的组成部件看成是 分离的物理实体，并有自己的独立活动。其中的变迁分布在模型中，它的激发只 同与之相联系的位置有关。同样，位置的变化也只取决于与之相联系的变迁，这 符合分布系统的特点，反映了物理上真正的并行通常库所表示活动，而变迁则 第7 页 国防科学技术大学研究生院工学硕士学位论文 表示活动间的转移但也有用变迁来表示活动，库所表示活动使能条件的做法。 如文献【5 l 】采用工作流网元素扩展时间属性，得到集成业务过程时间约束的工作流 模型时间约束工作流网( t c w f - n e t s ) ，以保证工作流执行的时间协调。 然而，传统的p e t r i 网不适合直接用于较复杂的工作流过程模型的建立，因此 使用改进的p e t r i 网建立工作流模型也是工作流过程模型研究的一个热点。基于这 一点，本文试图寻找一种结构简单，便于理解，且能有效的描述工作流特征的改 进的p e t r i 网模型。基于这个p e t r i 网模型，本文将设计实现一种支持该模型建模、 仿真和验证的工具。 如果将模型检验技术应用于工作流系统中，能够有效的提高验证质量并降低 设计周期和研发成本，可以近早的发现设计中的缺陷，可在建模阶段检验正确性， 而无需等到测试阶段。对于工作流而言，其模型空间为无穷状态空间，而模型检 验技术则适用于有穷状态空间。为确保模型检验技术能适用于工作流模型，本文 在设计工具的验证模块，需要通过一定的技术手段实现从有穷状态空间到无穷状 态空间的转换。考虑到模型检验的状态空间问题，本文还将完成从无穷状态空间 到有穷状态空间的转换，以及针对所建立的模型找出构造状态空间的算法。 1 5 本文贡献 综合1 4 节所提出的问题以及对研究重点的分析，本文以下章节将主要完成下 面三项工作： ( 1 ) 针对8 6 3 项目“面向金融领域的分布式工作流关键技术及应用框架”对 于工作流仿真的需求，本文基于p e 仃i 网具有良好的数学定义和强大的描述能力以 及能够有效支持仿真及形式化验证的特性，提出一种支持工作流性能分析的扩展 层次有色p e t d 网( e h c p n ) 模型。 ( 2 ) 基于e h c p n 模型设计并实现一个支持工作流建模、仿真和验证的集成 环境：w f - p t m s e ，实现对工作流e h c p n 模型的编辑建模、性能分析以及关于 时态逻辑属性的正确性检查。 ( 3 ) 在e h c p n 模型的基础上，提出状态组构造算法，并成功的运用到 w f - p 厂r m s e 集成环境的模型检验器中，该方法能够较为高效的构造验证所需的状 态空间，有效的支持工作流e h c p n 模型的验证。 1 6 大纲 本文继引言之后，第二章介绍论文中涉及的相关知识，首先对工作流以及工 作流管理系统的基本概念进行介绍，并简介工作流模型及其分类，其中主要介绍 第8 页 国防科学技术大学研究生院工学硕士学位论文 过程模型的组成；然后讨论模型检验、时态逻辑和可达性分析等相关知识。接着 在论文第三章，通过对p e t r i 网的介绍，逐步导出扩展层次有色p e t r i 网( e h c p n ) 的概念；通过对现有工作流模型的语法及语义的分析，研究现有的工作流模型向 基于e h c p n 的工作流模型转换的规则。第四章基于e h c p n 模型设计并实现了一 个支持工作流建模仿真和验证的集成环境：w f p t m s e 。w f - p i m s e 集成环境具 有可视化的建模环境，能够对工作流的e h c p n 模型进行性能分析，并对用户输入 的时态逻辑属性进行正确性检验。第五章使用w f p t m s e 仿真验证集成环境对商 场收银管理系统等多个案例进行性能分析和模型检验，验证结果表明了e h c p n 模 型具有强大的描述能力以及w f 删s e 仿真验证集成环境的可行性，其中 w f - p t m s e 的模型检验器所采用的状态组空间构造算法能够有效的支持工作流 e h c p n 模型的验证。最后总结全文工作，确定下一步工作计划。 第9 页 国防科学技术大学研究生院工学硕士学位论文 第二章背景知识 本章着重介绍论文中涉及的各种技术。首先介绍工作流，工作流管理条统以 及工作流模型的概念。然后对模型检验、时态逻辑和可达性分析的相关知识做概 要性介绍。 2 1 工作流概述 2 1 1 工作流及工作流管理系统 工作流的概念起源于生产组织和办公自动化领域。它是针对日常工作中具有 固定程序的一系列活动而提出的一个概念。提出的目的是通过将工作分解成定义 良好的任务、角色，按照一定的规则和过程来执行这些任务并对它们进行监控， 达到提高办事效率、降低生产成本、提高企业生产经营管理水平和企业竞争力的 目标。在计算机网络技术和分布式数据库技术迅速发展、多机协同工作技术日臻 成熟的基础上，于2 0 世纪8 0 年代中期发展起来的工作流技术为企业更好的实现 这些经营目标提供了先进的手段。工作流技术一出现马上就得到广泛的重视和研 究。至今，工作流管理技术已成功的运用到医院、保险公司、银行等行业，然而 它更重要的应用还是在工业领域，特别是制造业领域中。 工作流管理联盟对工作流的定义是1 9 】：工作流是一类能够完全或者部分自动执 行的经营过程，它是根据一系列过程规则，文档、信息或任务能够在不同的执行 者之间进行传递与执行。工作流的最根本目的是在正确的顺序下，各项任务由最 合适的人员执行，使得业务过程的执行效率最大化。 目前，在全球范围内，对工作流的技术研究以及相关的产品开发进入了非常 繁荣的阶段，更多更新的技术被集成进来。文档管理系统、电子邮件、移动式计 算、i n t e m e t 服务等都已被容纳到工作流管理系统之中。工作流产品的市场每年以 两位数字的速度迅猛增长。此外，随着计算机技术的发展，工作流产品的供应商 及时将新技术融入工作流中，提高产品性能，使得工作流技术得到不断完善。作 为支持企业经营过程重组( b u s i n e s sp r o c e s sr e e n g i n e e r i n g ，b p b ) 和经营过程自动 化( b u s i n e s sp r o c e s sa u t o m a t i o n ，b p a ) 的一种手段，工作流技术的研究应用日益 受