（计算机软件与理论专业论文）基于时序逻辑的有效性控制的研究与应用.pdf

ad i s s e r t a t i o ns u b m i t t e dt og u a n g d o n g u n i v e r s i t yo ft e c h n o l o g y f o rt h ed e g r e eo fm a s t e ro f e n g i n e e r i n gs c i e n c e u s i n gt e m p o r a ll o g i ct oc o n t r o lv a l i d i t yo f t e m p o r a li n f o r m a t i o n c a n d i d a t e ：l i ul e i s u p e r v i s o r ：a s s o c i a t ep r o f x uh a i s h u i m a y2 0 1 0 f a c u l t yo fc o mp u t e r g u a n g d o n gu n i v e r s i t yo ft e c h n o l o g y g u a n g z h o u ，g u a n g d o n g ，p r c h i n a ，5 10 0 9 0 摘要 摘要 随着社会经济的快速发展，国家及各级地方政府对教育行业的投入越来越大，教 育采购的规模也逐年扩大，这样需要一套信息化的措施来提高政府采购的执行效率。 政府采购过程涉及单位众多，如何保证采购业务信息规范高效可控地流经各部门是采 购过程信息化要解决的首要问题，而且采购业务信息与时间有紧密关系，比如标书发 标之后的三天才可以投标等。这样对采购系统的的时间管理就有较高的要求。在工作 流应用方面，随着企业竞争的日趋激烈，企业的业务过程也动态多变，要求控制业务 信息实时地流经企业。这样原来的工作流系统已不适应现今的企业需求。时间信息的 有效管理已经成为工作流技术推广应用的主要障碍，因此研究工作流的时间信息管理 有重要意义。 本文基于协议采购系统研究如何有效地控制采购系统中的与业务相关的时间信 息，协议采购系统是借助于工作流技术实现的。在工作流时问管理中，时间信息的建 模、验证和分析是最基础、最核心的问题。为了解决协议采购系统中时间信息的建模 和验证问题，我们引入了模型检测思想，利用模型检测技术来为协议采购系统的时间 信息建模，提出了时钟k r i p k e 迁移系统。时钟k r i p k e 迁移系统是由k r i p k e 迁移系统 改进而来的，我们在原来模型的基础上增加了局部时钟和全局时钟，而且引入了特殊 的迁移关系t i c k 来表示时钟的运行，这样时钟k r i p k e 迁移系统就可以用来建模工作流 系统的时间信息。随后我们又分析了该模型相对于其他模型的优缺点。为了验证采购 系统中的时间约束，首先提出了有效性的概念，给出了有效性约束的三种类型，然后 利用时序逻辑c t l 建立了有效性约束的模型。由于c t l 的语义可以在状态迁移系统上 进行解释，这样建模方法和验证方法就统一起来了。由于相关文献已经给出了工作流 过程描述语言w p d l 描述的工作流模型到k r i p k e 迁移系统的转换方法，这样也就很容 易建立基于时钟k r i p k e 迁移系统的工作流模型，这就使得该方法更贴近于实用。最后 给出了协议采购系统的一个实例，利用模型检测工具s m v 验证了该实例的有效性约束， 验证结果表明我们提出的方法是可行的。这样我们就把模型检测技术应用到了工作流 系统中，对探索利用模型检测思想来对工作流时间信息建模与验证做了有益的尝试。 广东工业大学硕士学位论文 关键词：工作流；模型检测；时序逻辑；状态迁移系统 i i a b s t r a c t a b s t r a c t 舡t h e r a p i dd e v e l o p m e n to fe c o n o m y , t h es t a t ea n dl o c a lg o v e r n m e n t s i n v e s tm o r ea n d m o r ec a p i t a li ne d u c a t i o n a ne l e c t r o n i cp r o c u r e m e n ts y s t e mi sr e q u i r e dt oi m p r o v et h e e f f i c i e n c yo ft h eg o v e r n m e n t a lp r o c u r e m e n t o na c c o u n tt ot h ep r o c e s s e so fg o v e r n m e n t a l p r o c u r e m e n tw h i c hi n v o l v em a n yd e p a r t m e n t s ，w em u s te n s u r et h a tt h eb u s i n e s si n f o r m a t i o n p a s so nf r o mo n ed e p a r t m e n tt oa n o t h e rs y s t e m a t i c a l l ya n de f f i c i e n t l y f u r t h e rm o r e ，t h e s e b u s i n e s si n f o r m a t i o nr e l a t et ot i m es t r i c t l y f o re x a m p l e ，t e n d e rd o c u m e n tc a nn o tb eo p e n e d u n t i lt h r e ed a y sl a t e ra f t e ri ti si s s u e d s ot h i sp r o c u r e m e n ts y s t e mh a sar i g i dr e q u i r e m e n to n t i m em a n a g e m e n t o nt h eo t h e r , t h ec o m p e t i t i o na m o n ge n t e r p r i s e si s s of e r c et h a tt h e b u s i n e s sp r o c e s si so f t e nc h a n g e da n dn o ts t a b l e s ot h ep r e v i o u sp r o d u c t so fw o r k f l o wa r e n o ts u i t a b l ef o rt h i sn e ws i t u a t i o n t h et i m em a n a g e m e n to f w o r k f l o ws y s t e mh a sb e c a m e t h em a i no b s t r u c t i o nt op r o m o t et h ea p p l i c a t i o no fw o r k f l o w t h i sp a p e rb a s e so nt h eg u a n g d o n ge d u c a t i o nd e p a r t m e n tp r o c u r e m e n ts y s t e m , a n d w el o o kf o ram e t h o dt oc o n t r o lt h et e m p o r a lv a l i d i t yo ft h ei n f o r m a t i o no fb u s i n e s sp r o c e s s o nt i m em a n a g e m e n to f w o r k f l o ws y s t e mt h em o s tp r i m i t i v ea n dc r u c i a lp r o b l e mi sh o wt o m o d e lt h et e m p o r a li n f o r m a t i o no fw o r k f l o wa n dv e r i f yt h e m i no r d e rt om o d e lt h e t e m p o r a li n f o r m a t i o no fw o r k f l o w , w ea d o p t e dm o d e lc h e c k i n gt e c h n o l o g ya n dp r e s e n t e dt h e c l o c kk r i p k et r a n s i t i o ns y s t e mt od e s c r i b et h et e m p o r a li n f o r m a t i o n c l o c kk r i p k e t r a n s i t i o ns y s t e m , w h i c ho r i g i n a t e df r o mk r i p k et r a n s i t i o ns y s t e m , w a sa d d e db yt w om o r e e l e m e n t s ，c l o c ka n dl o c a lc l o c k t h ec l o c ki su s e dt op r e s e n tt h es y s t e mt i m e ，a n dt h el o c a l c l o c kp r e s e n tt h el o c a lt i m eo fe v e r ys t a t eo ft r a n s i t i o ns y s t e m as p e c i a lt r a n s i t i o nr e l a t i o n t i c kw a sa d h i b i t e dt od e s c r i b et h er u n n i n go fc l o c k s ot h ec l o c kk r i p k et r a n s i t i o ns y s t e m c a nu s e dt om o d e lt h et i m ei n f o r m a t i o no fw o r k f l o ws y s t e m t h ea d v a n t a g e sa n d d i s a d v a n t a g e so ft l l i sm o d e lc o m p a r e dt oo t h e rm o d e l sa r ea l s oa n a l y z e d i no r d e rt ov e r i f y t h et i m ev a l i d i t yc o n s t r a i n t ，w ef i r s tg i v et h ed e f m i t i o no ft i m ev a l i d i t y , p r e s e n t e dt h r e ek i n d s o ft i m ev a l i d i t yc o n s t r a i n t ，a n dt h e ng i v et h em o d e lo ft i m ev a l i d i t yc o n s t r a i n td e s c r i b e db y c t l t h es e m a n t i c so fc t lc a nb ee x p l a i n e do ns t a t et r a n s i t i o ns y s t e m , s ot h em e t h o d so f m o d e la n dv e r i f ya r ec o n s i s t e n t f i n a l l y ，t h em o d e lc h e c k i n gt o o ls m v i su s e dt ov e r i f ya n i n s t a n c eo fp r o c u r e m e n ts y s t e m , a n dt h er e s u l tp r o v e dt h a tt h em e t h o dw ep r e s e n t e di s t e a s i b l e ! 1 1 广东工业大学硕士学位论丈 k e y w o r d s ：w o r k f l o w ；m o d e lc h e c k i n g ；t e m p o r a ll o g i c ； i v 目录 目录 摘要一：i a b s t r a c t i i i 目录v c o n t e n t s v i i i 第一章绪论1 1 1 研究背景l 1 1 1 工作流系统中的时间问题1 1 1 2 政府教育采购1 1 2 国内外研究现状2 1 2 1 基于工作流图的方法2 1 2 2 基于p e t r i 网的方法3 1 2 3 基于时序逻辑的方法4 1 2 4 时间信息建模方法的比较4 1 3 论文内容和组织结构5 1 3 1 论文的主要内容5 1 3 2 论文的组织结构5 1 4 本章小结6 第二章工作流概述7 2 1 工作流的定义7 2 2 工作流的时间模型8 2 3 工作流时间管理1 0 2 3 1 时间信息建模l l 2 3 2 模型实例化阶段1 2 2 3 3 实例运行阶段l2 2 4 本章小结1 2 第三章时序逻辑l3 v 广东工业大学硕士学位论文 3 1 时序逻辑概述13 3 2 线性时序逻辑l t l 。1 3 3 2 1l t l 的语法1 4 3 2 2l t l 的语义1 4 3 3 计算树逻辑c t l 1 5 3 3 1c t l 的语法15 3 3 2c t l 的语义。1 6 3 4 本章小结16 第四章协议采购系统及其w p d l 描述1 7 4 1 协议采购系统17 4 1 1 协议采购系统概述1 7 4 1 2 协议采购系统业务流程1 7 4 2 协议采购流程w p d l 描述2 l 4 2 1w p d l 概要介绍2 l 4 2 2 业务流程w p d l 描述2 4 4 3 本章小结2 8 第五章协议采购系统的逻辑描述2 9 5 1 时钟k r i p k e 迁移系统2 9 5 1 1 时钟k r i p k e 迁移系统的结构2 9 5 1 2 时钟k r i p k e 迁移系统的特点3 0 5 2 基于时钟k r i p k e 迁移系统的采购系统描述3 l 5 2 1 工作流模型向时钟k r i p k e 迁移系统的转换3 1 5 2 2 协议采购系统的时钟k r i p k e 迁移系统描述3 2 5 3 本章小结3 6 第六章有效性约束的建模3 7 6 1 有效性的定义3 7 6 2 有效性约束及其建模3 7 6 3 本章小结3 9 第七章有效性约束的验证4 0 7 1 模型检测概述4 0 目录 7 2s m v 系统4 l 7 2 1s m v 概述4 l 7 2 2s m v 语言4 2 7 3 协议采购流程有效性约束的实例验证4 6 7 4 本章小结4 9 总结与展望5 0 l 总结5 0 2 展望一5l 参考文献一5 2 攻读学位期间发表的论文5 5 独创性声明5 6 蓟【谢5 7 v i i 广东工业大学硕士学位论文 c o n t e n t s a b s t r a c t ( c h i n e s e ) i a b s t r a c t i i i c o n t e n t s ( c h i n e s e ) 。v c o n t e n t s v i i i c h a p t e r 1i n t r o d u c t i o n 1 1 1 b a c k g r o u n d “1 1 1 1t i m ei n f o r m a t i o ni nw o r k f l o w 1 1 1 2g o v e r n m e n tp r o c u r e m e n ti ne d u c a t i o n 1 1 2r e l a t e dr e s e a r c h 2 1 2 1t i m em o d e l i n gb a s e do nw o r k f l o wg r a p h 2 1 2 2t i m em o d e l i n gb a s e do np e t r in e t 3 1 2 3t i m em o d e l i n gb a s e do nt e m p o r a ll o g i c 4 1 2 4c o m p a r i s o na m o n gt i m em o d e l i n g s 4 1 3r e s e a r c hc o m e ma n dp a p e rs t r u c t u r e 5 1 3 1r e s e a r c hc o n t e n t 5 1 3 2p a p e rs t r u c t u r e 5 1 4c h a p t e rs u m m a r y 一6 c h a p t e r 2w o r k f l o w ”7 2 1d e f i n i t i o no f w o r k f l o w 一7 2 2t i m em o d e lo fw o r k f l o w 8 2 3t i m em a n a g e m e n t 1 0 2 3 1m o d e lb u i l d i n g 1 1 2 3 2m o d e li n s t a n t i a t i o n 1 2 2 3 3m o d e le x e c u t i o n 1 2 2 4c h a p t e rs u m m a r y 1 2 c h a p t e r 3t e m p o r a ll o g i c 1 3 3 1t e m p o r a ll o g i co v e r v i e w “1 3 3 2l i n e a r - t i m et e m p o r a ll o g i cl t l 1 3 3 2 1s y n t a xo fl t l 。1 4 v i i i c o n t e n t s 3 2 2s e m a n t i c so f c t l ：1 4 3 3c o m p u t a t i o nt r e el o g i cc t l 15 3 3 1s y n t a xo f c t l 1 5 3 3 2s e m a n t i c so f c t l 1 6 3 4c h a p t e rs u m m a r y 1 6 c h a p t e r4g o v e r n m e n tp r o c u r e m e n ts y s t e ma n d i t sd e s c r i p t i o n 1 7 4 1g o v e r n m e n tp r o c u r e m e n ts y s t e m 1 7 4 1 1b a c k g r o u n d 。1 7 4 1 2b u s i n e s sp r o c e s s 1 7 4 2d e s c r i p t i o no f p r o c u r e m e n t 2 1 4 2 1i n t r o d u c t i o nt ow p d l 2 1 4 2 2d e s c r i p t i o nb yw p d l 2 4 4 3c h a p t e rs u m m a r y 2 8 c h a p t e r5l o g i cm o d e lo fp r o c u r e m e n ts y s t e m 2 9 5 1c l o c kk r i p k et r a n s i t i o ns y s t e mc k t s 2 9 5 1 1s t r u c t u r eo fc k t s 2 9 5 1 2c h a r a c t e r i s t i c so f c k t s 一3 0 5 2p r o c u r e m e n ts y s t e md e s c r i b e db yc k t s 3 1 5 2 1c o n v e r t i o nm e t h o dt oc k t s 3 1 5 2 2d e s c r i p t i o no f p r o c u r e m e n tb a s e do nc k t s 3 2 5 3c h a p t e rs u r r m a a r y 3 6 c h a p t e r 6t i m ev a l i d i t yc o n s t r a i n tm o d e h n g 3 7 6 1d e f i n i t i o no f t i m ev a l i d i t y 3 7 6 2t i m ev a l i d f f yc o n s t r a i n t 3 7 6 3c h a p t e rs u m m a r y 3 9 c h a p t e r 7v e r i f i c a t i o no ft i m ev a l i d i t yc o n s t r a i n t 4 0 7 1m o d e lc h e c k i n g 4 0 7 2s m vs y s t e m 4 1 7 2 1i n t r o d u c t i o nt os m v 4 1 7 2 2s m v l a n g u a g e 4 2 7 3v e r i f y i n gp r o c u r e m e n ts y s t e m 4 6 7 4c h a p t e rs u m m a r y 4 9 s u m m a r ya n de x p e c t a t i o n 5 0 i x 广东工业大学硕士学位论文 1s u m m a r y 5 0 2f u r t h e rw o r ke x p e c t a t i o n 5 1 r e f e r e n c e s 5 2 p u b l i s h e da c a d e m i cp a p e r sd u 订n ga p p u c a t i o nf o rm a s t e rd e g r e e 5 5 o r i g i n a ls t a t e m e n t 5 6 t h a n k s 5 7 x 第一章绪论 1 1 研究背景 第一章绪论弟一早三百t 匕 1 1 1 工作流系统中的时间问题 2 0 世纪8 0 年代中期发展起来的工作流技术，在企业的同常经营与生产管理中起到 了越来越重要的作用，为企业完成经营目标提供了有效的手段。至今，工作流管理技 术已成功地应用于医院、保险公司、金融等行业，特别是在制造业领域，发挥着越来 越大的作用【i 】。随着工作流技术的发展，出现了各种各样的工作流产品。然而近年来， 瞬息万变的市场环境和企业激烈的竞争会导致业务流程的动态多变和业务管理的低 效，能否有效处理时间及时序约束问题已经成为工作流系统成功实施的关键【：】。实际业 务过程大多具有时间约束，时间违反将增加业务成本，所以，实施工作流需要处理时 间问题，保证执行过程中满足时序约束。因此研究工作流时间管理对丰富工作流系统 管理功能，提高系统柔性及促进工作流技术应用都有重要的实际意义。 时间在业务过程管理中起着十分重要的作用。在工作流模型建立阶段，建模者需 要某种方式来表现业务过程中与时问相关的信息，并检查该模型的可行性。在模型运 行阶段，过程管理者需要某种机制来提前知道可能会产生的时间约束冲突，还需要监 控整个流程的执行过程【，】。过程参与者也需要知道分配给他们的任务的紧急程度，以便 他们自己制定合理的工作计划。当时间约束产生冲突时，工作流系统还要启动异常处 理机制以便处理由此产生的异常。异常处理完成后，工作流系统还要恢复到一致性状 态。 1 1 2 政府教育采购 随着社会经济不断快速发展，国家以及各级地方政府对教育行业的投入不断加大， 教育采购的规模逐年扩大，体现出了较强的行业性特点。其采购过程无论在数量上， 还是在品种类型上都表现出：批次多、品目单项数量少但采购品种多样、要求的到货 广东工业大学硕士学位论文 时问短等特点。国家也出台了相应的法规，要求此类采购必须按照国家相应的法律法 规来执行。但由于此类采购过程涉及单位众多，而且按照国家有关文件要求，政府采 购必须要规范、公平、高效地执行，传统的纸质申报过程无论在时间要求上还是在信 息透明度上都不能满足要求，所以有必要采用信息化的技术来使采购流程自动化，采 购信息透明化。 由于政府采购要涉及众多单位，如何保证信息在这些单位之间及时有序规范地流 动，是采购流程信息化要解决的首要问题。而且采购过程中的大多业务与时间有紧密 关系，如政府发布的招标公告，都会有一个竞标的时间区间，超过这个时问区间，该 标书就视为无效的。再比如，为提高政府工作的效率，有些文件在提交或审核过程中 会有一个时间限制，比如在什么时间之前必须提交或审核完成。这些业务都与时间有 紧密关系。目前，我国的法律还不完善，政府采购的法规也在不断的更新，这就要求 信息化的采购系统还要满足采购流程和业务时间要求的柔性变化。由此看来，如何控 制采购流程中信息的时间有效性，是采购过程信息化要解决的关键问题。 1 2 国内外研究现状 时间管理是研究工作流执行的时间维计划，估计活动的执行延迟，避免活动的执 行违反时序约束，监视整个工作流的执行进程，以及出现时序违反时的异常处理。时 间管理的关键在于时间信息的有效建模，这是一个国际性的难题，国外已经开展了相 关的研究，国内的研究主要着重于工作流建模方法和工作流实现技术，对业务过程的 时间管理尚未进行专门的讨论 2 j 。 时间建模是在工作流模型中嵌入时间信息，扩展工作流模型使其包含时间因素，从 而利用时间信息来进行时间有关的计算。如计算活动执行时间与过程延迟，验证时序 约束一致性，监控整个工作流的执行进程等。下面我们主要介绍几种不同的时间信息 建模方法。 1 2 1 基于工作流图的方法 e d e r 基于赋时活动图，建立了包含活动时间属性的工作流模型删。提出了固定日 期约束以及时间距离约束，并将所有的时间约束换算为活动执行结束的时间点。每一 个赋时活动节点1 有三个时间属性n d ，e n l ，它们分别表示刀的执行延迟最早完成 2 第一章绪论 时间最晚完成时间，如图1 1 所示。e d e r 将工作流中的时间管理划分为三个阶段：模 型建立阶段、实例化阶段和运行阶段，并利用时间工作流模型分别给出了这三个阶段 的时间信息的计算方法，如何保证时序约束与活动执行过程的一致性，以及如何监控 整个工作流的执行进程等。 a c t i v i t yn a m ea c t i v i t yd u r a t i o n n n d e a r l i e s tf i n i s hl a t e s tf i n i s h 1 1 m en eo币m en l 活动标识甩活动延迟，d最早完成时间刀e最迟完成时间n 三 图1 - 1 赋时活动节点 f i g l - la c t i v i t yn o d eo fa t i m e dw o r k f l o wg r a p h m a r j a n o v i c 基于好结构的( w e l ls t r u c t u r e d ) i 作流模型，利用延迟间隔描述活动执行 延迟的不确定性，定义了有限延迟约束、截至期限约束、时间距离约束【s 】。任务f 的延 迟约束d ( i ) = 【肌( f ) ，m ( f ) 】，m ( i ) m ( i ) 表示f 的最大最小延迟时间。显然有m ( i ) m ( f ) ， 且若所( f ) = m ( f ) ，则表示活动f 有精确的执行延迟。m a r j a n o v i c 提出了延迟空间和实例 空间的概念，来图形化表示时问约束1 6 1 。还给出了控制点( c o n t r o lp o i n t s ) 的概念，来描 述工作流运行过程中时序约束的动态验证，这样潜在的时序违反就可以被提前发现， 从而可以采取应对措施来避免时序约束违反的发生。 1 2 2 基于p e t r i 网的方法 p e t r i 网利用触发延迟、保持延迟和使能延迟等时间表示形式描述不同语义的实时 系统1 7 - 9 ，例如为库所变迁扩展时间参数对，为t o k e n 赋予时间戳( t i m e s t a m p ) 表示业务 实例的全局生命时间 t o l 。l i n g 通过扩展基本网系统包含业务过程的时间因素，提出了 时间工作流网，并将活动执行时间映射为工作流网的变迁时间对，修改工作流网的分 析方法如活性、安全性和合理性来分析时间约束工作流的行为性质【t 一j 2 l 。a d a m 以p e t r i 网为建模分析工具，基于“操作元语”语义框架，将任务划分为操作集和任务元语集， 全面描述任务在整个工作流执行中所遍历的五种状态：初始态、执行态、完成态、提 交态和退出态；并借助于库所变迁时间对以及t o k e n 时间戳来建模任务间的时序依赖 约束，包括业务实例的到达时间和任务可执行时间范围等邮l 。 广东工业大学硕士学位论文 1 2 3 基于时序逻辑的方法 该方法由国内的王远、范玉顺提出0 4 - 1 5 1 。通过利用一阶逻辑来描述赋时工作流图的 六种基本结构，从而给出工作流系统的一阶逻辑模型。该模型在一个l ( r i p k e 结构 m = ( s ，s o ，r ，三) 上进行语义解释，其中，s 表示工作流系统运行的状态集合，品表示 工作流运行的初始状态，r 表示随着时间的变化工作流系统状态的变迁关系，三为映 射：s _ 2 肿，其中，彳尸为系统中所有原子命题的集合，三( s ) 表示在状态s 下成立的 原子命题的集合。利用时序逻辑来描述时序约束，采用模型检测方法进行验证，这样 就使得工作流时间建模与验证方法得到了统一，而且有模型检测工具的支持，在工程 实践中易于实现和应用。 1 2 4 时间信息建模方法的比较 工作流时间信息建模方法还缺乏统一的规范和标准，已有的时间建模与分析方法主 要基于工作流图和p e t r i 网。各种建模方法所考虑的时序约束和采用的验证方法都不同， 具有很大的局限性。而且各种建模方法要么侧重于过程模型验证，要么侧重于时序一 致性验诳2 1 ，全面的工作流控制描述，应该考虑过程模型与时序约束的一致性。时间信 息的建模与分析是在工作流过程模型基础之上的 2 1 ，为了描述复杂的时序约束信息，以 及保证业务过程与时序约束的一致性，需要一套将过程建模与时间建模统一起来的方 法。 e d e r 和m a r j a n o v i c 提出的时间信息建模方法，侧重于业务过程的时间信息的计算 和验证，但缺乏对集成了时间约束的工作流模型正确性验证的有效手段，比如工作流 模型的合理性、活性和有界性等。 基于p e t r i 网的时间信息建模方法主要有两个问题1 5 1 ：一是没有统一的建模框架， 无法满足工作流系统多种性质的验证需要；二是无法指导工作流模型的设计工作，比 如要设计一个给定性质的工作流模型，现有方法就不能满足此需求。而且基于经典p e t r i 网建模，会有状态爆炸问题，难以描述较大规模的系统，但具有广义时问约束的面向 对象p e t r i 有可能会获得应用。 王远和范玉顺提出的基于时序逻辑的建模方法将时间信息建模方法和验证方法统 一起来了，但主要侧重于时序约束一致性验证，没有将过程模型与时序约束结合起来， 4 第一章绪论 而且缺乏工作流运行过程中时序约束动态验证的有效手段。 1 3 论文内容和组织结构 1 3 1 论文的主要内容 本文根据状态迁移系统和k r i p k e 结构，提出了适合描述工作流时间信息的时钟 k r i p k e 迁移系统模型，时钟k r i p k e 迁移系统m = ( y ，z o ，a c t ，t ，l ，彳尸，c ，l c ) 是一个八 元组，其中，v = ( 岛，l c i ) h s ，l c i 】l c ，f = o ，l ，2 ) ，s 为系统所有状态的集合， l c 为所有本地时钟的集合；v o = ( ，c o ) ，s o 是系统的初始状态，z c o 】是初始状态 对应的时钟；a c t 是系统活动标记的集合；t 是迁移关系的集合，t = tu