没有合适的资源?快使用搜索试试~ 我知道了~
工作流模型切片方法的验证效果
可在www.sciencedirect.com在线获取理论计算机科学电子笔记295(2013)79-93www.elsevier.com/locate/entcs工作流验证的模型切片方法Fazle Rabbi Hao Wang Wendy MacCaull Adrian Rutle加拿大圣弗朗西斯泽维尔大学逻辑与信息中心{rfazle,hwang,wmaccaul,arutle}@ stfx.ca摘要工作流程系统提高了生产力和服务质量;然而,工作流程模型中的缺陷可能会产生严重的后果。虽然模型检查技术可以用来验证工作流模型的正确性,但这些技术通常来自状态爆炸问题。我们提出了一个模型切片算法与正式证明,以解决这个问题。该算法集成到我们的NOVA工作流程框架中,便于设计,验证,执行和错误处理。实验结果表明,该算法在状态空间、存储空间和时间上都有较好的验证效果.关键词:模型切片,形式化验证,工作流建模,模型检测,线性时序逻辑1介绍工作流协调各种参与者执行的活动,例如,人、机器人或软件组件,以实现业务目标。目前,工作流模型经常被用来描述分布式和异构环境中软件组件的行为,这些环境具有并发、资源共享和同步等特征。在这样的协作环境中,工作流系统可以用于基于描述组件行为的工作流模型来控制运行时执行和服务编排。今天的许多然而,未经验证的复杂工作流程模型的最终需要模型检查或其他类似的验证技术来确保这些过程模型表现出所需的行为。模型检测算法的时间复杂度取决于转换系统的大小,其在变量、并发组件和通道的数量上是指数的。这个问题通常被称为状态爆炸问题[4]。虽然目前的模式1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.04.00780F. Rabbi et al.理论计算机科学电子笔记295(2013)79尽管跳棋比它们的前辈强大得多,但它们仍然经常受到这个问题的困扰。在过去的十年里,在这一领域进行了大量的研究。虽然有许多技术来优化模型检查算法,例如,部分降阶(POR)[15]、基于对称的降阶[9]、称为模型抽象的一类技术[4]对于缓解状态爆炸问题也非常重要。 这些技术抽象掉了无关的细节。在将系统模型输入到模型检查器之前验证属性有两种类型的模型抽象技术:数据抽象,它使用一组较小的数据值来表示系统的实际值;模型切片,它消除了不会影响被验证属性的真值的模型组件。在本文中,我们专注于后者的技术。虽然软件程序切片问题[7]是一个研究得很好的主题,但对于正式图形语言的切片工作相对较少,对于工作流建模语言的工作就更少了 本文发展并集成了抽象模型,将技术融入工作流程框架。我们的团队开发了NOVA工作流程,这是一个用于工作流程设计、验证、执行和错误处理的框架使用NOVA编辑器,可以图形化地为许多应用领域建模工作流程,例如,医疗保健协议,商业支持,cesses,scienti-fic工作流,等等,使用可补偿工作流建模语言(CWML)[17]并为任务编写业务逻辑这些工作流模型由NOVA引擎执行。在执行之前,使用NOVA Translator [17]将工作流模型自动转换为DVE,即DiVinE [3]模型检查器的输入语言虽然我们可以对一个大型工作流程建模并将其转换为模型检查程序,但验证所需的时间和空间有时是不可接受的。我们的实验表明,尽管Divine配备了POR和许多其他算法,但它需要大量的内存和时间来验证大型模型。在本文中,我们提出了一个模型切片算法的工作流构造使用CWML。该算法已在NOVA Translator中实现。它采用一个工作流模型和一个时序逻辑公式φ的具体化,并以一种保持和反映φ的真值的方式简化模型线性时态逻辑(LTL)是一个强大的工具,推理系统的属性随时间而变化。LTL是一种时态逻辑,除了经典的命题逻辑运算符之外,它还使用时态运算符:always(G),eventually(F),直到(U),下一次(X)。 其完整的语义可以在[4]中找到。 的本文提出的切片算法适用于LTL−X公式(不包含X算子的LTL公式子集[4])。我们给出了详细的证明的等价性的原始模型和约简模型所产生的算法。此外,我们展示了如何有效地减少所提出的方法的状态空间的大小。我们希望所提出的算法可以很容易地应用于任何块结构的建模语言,例如,[8]。请注意,该算法处理的是工作流建模语言中常见的数据感知功能。我们展示了它的适用性,F. Rabbi et al.理论计算机科学电子笔记295(2013)7981CWML~st模型M序列化文本M的表达Text2TST任务树λ简化CWML模型M'骨化M'的简化TST2Text简化任务树λ'transl.DiVinE型号D神是的|没有切片LTL_X公式一个相当大的医疗工作流程模型的方法的有效性。图1显示了本文提出的方法中不同步骤的概述。我们的工作流模型M由CWML指定每个模型M被串行化为对应的文本表达式,该文本表达式对于w.r.t.定义2.2和2.3中的BNF我们使用Text2TST算法(参见算法1)来解析表达式并生成任务树(TST)λ。切片算法(参见算法2)用于将λ减小到减小的TSTλJ w.r.t.LTL−X公式φ。从简化的TSTλJ,TST2Text算法创建文本表达式,该文本表达式反过来将由NOVA Work Wavelow作为CWML模型MJ进行描述和可视化。的TST2Text算法不包括在本文中,因为它很简单。在第3.3节中,我们证明了模型M和MJ是关于t的口吃等价的。φ。Fig. 1.拟议办法第2节提供了一些背景资料。在第三节中,我们提出了模型切片算法,并证明了工作流模型M和相应的简化模型MJ的口吃等价性。第4节提出了一个现实的实验,一个真实世界的卫生服务提供模式。第5节将我们的方法与其他工作联系起来,第6节总结了本文并概述了未来的工作。research.2预赛CWML中的工作流模型由任务和连接这些任务的操作符组成某些任务的执行受到前提条件的保护,并且在执行时可能执行某些操作。我们首先回顾一些定义。定义2.1(项、先决条件和动作)项t递归地定义为BNFat::=c|χ|t<$At,其中r<$A∈{+,−,n,n},c是一个整数,χ是一个(自然)变量.一个前提条件是一个公式,定义为:::=t|当n ∈C∈{<,≤,>,≥,==}且n∈P∈{&&,n}时,n ∈ P. nac t iona是一个赋值,定义为α::= v = t; v称为受让人变量。我们滥用符号{α}来表示一组动作。可补偿任务可以在以后撤消或回滚其操作,如果需要的话,它的成功执行。在CWML中,可补偿的任务由82F. Rabbi et al.理论计算机科学电子笔记295(2013)79用t-演算算子[11]提供多种补偿方法t-calculus允许将可补偿的事务组合起来,以建立一个长期运行的业务事务,该事务将补偿作为其主要的错误恢复技术。一个可补偿的任务由原子可补偿的任务组成,这些任务由COM-pensabl e o ope r a p era p erac.定义2.2(可补偿任务)一个可补偿任务Tc是递归定义的,使用BNF确定为Tc::= τc|({T}Tc1{T}T),其中τc::=τid<${ατ,αb}c1Tcc2c2cτc是一个具有一组转发和补偿操作的原子可补偿任务一个面向对象和虚拟化的解决方案是数据库、内存和数据库的一个组成部分,∈{·,,×,S,A}是一个t-演算算子。 只有当Tc1 × Tc2时,Tc1,Tc2才分别有一个前提条件<$Tc1,<$Tc2.用于组合可补偿任务的运算符解释如下:•T1·T2(顺序):首先执行T1,然后执行T2。•T1和T2(并行):T1和T2将并行执行.如果其中一个被中止,另一个也将被中止。• T1 × T2(内部选择):只执行其中一个任务。• T1S T2(推测性选择):T1和T2将并行执行,最先到达目标的任务将被接受,另一个将被中止。•T1AT2(Alternative forwarding):如果满足以下条件,则首先执行T1T1被中止,T2将被执行以实现目标.一个任务可以包含可补偿任务和不可补偿任务,由操作符连接。定义2.3(任务)使用BNF递归地定义任务T为T::= τ|Tc|({T}T1T{T}T2)|{T}(T)+,其中τ::= id{α}是原子不可补偿的1 2任务有一组与之关联的操作{α},任务ID是任务的名称,此外,T∈ {·,λ,×,λ}是一个二元算子,T+是一个应用于T的一元算子.只有对T1×T2,T1<$T2和T+,T1,T2,T才分别有一个前提条件<$T1,<$T2,<$T用于合并任务的运算符解释如下:•T1·T2(顺序):首先执行T1,然后执行T2。•T1和T2(并行):T1和T2将并行执行.•T1×T2(独占选择):两个任务中的一个将被执行。•T1和T2(选择):T1或T2或两者并行执行.• T+(循环):只要前提条件为真,T就被执行一次或(指定的)有限次。CWML中的工作流模型M是具有一个输入和一个输出条件的任务。M的底层语义由Petri网给出;参见[16]中每个任务的底层Petri网。M的状态由其底层Petri网的标记决定。M中的路径定义如下。F. Rabbi et al.理论计算机科学电子笔记295(2013)7983×B定义2.4(路径)给定一个工作流模型M,路径π=(s0→s1→s2→... )是一个状态序列。在M中执行一个任务而引起的从一种状态到另一种状态的转换。 路径π的长度是π中状态变化的次数。注意,由(s0→s1 ...Sτij−→sj+1 ... )我们表示任何涉及执行任务τi。我们用πk表示长度为k的路径。 这项任务造成状态改变的索赔可以是不可赔偿的,也可以是可赔偿的。因此,我们认为,在3.3节中,我们能够通过对路径的长度使用结构归纳来证明口吃等价性,而不管所使用的任务类型3工作流切片在本节中,我们首先介绍一种从CWML模型创建TST的算法。然后,我们提出了我们的切片算法,并证明了使用该算法来减少工作流模型将产生一个模型,是口吃相当于原来的模型。3.1任务树CWML指定的工作流模型具有图形结构。这些结构被序列化为有效的文本表达。定义2.2和2.3这些表达式被解析并表示为任务语法树(TST),其中非叶节点表示运算符,叶节点表示原子(可能是可补偿的)任务(参见图2)。Text2TST(参见算法1)概述了如何从文本表达式生成TST,它是从标准解析过程[12]改编而来的注意只有非叶节点(运算符)的×(XOR)或×(OR)或或+具有非空的前提条件。(内部选择)你好,s,,τ1,ψτss sss,τ,s,zC1ssssC2、、τ{α}τ{α},sz1τ12τ2τc1{ατc1bτc1}τc2{ατc2τc2}(a) 使用原子uncom的树-可支付的任务(b) 具有原子可补偿任务的图二. 工作流语法树3.2切片算法切片算法(见算法2)根据LTL公式减小了工作流程模型的大小,并进行了验证。给定一个工作流,我们基于我们希望验证的LTL公式φ来降低其TSTλ。在工作流切片算法中,我们首先确定φ中出现的变量,并将它们存储在集合E(保留元素)中。然后,集合E将被递归地扩展为任务、先决条件、变量和w.r.t.可见的动作。发生的变量×S、}{α}{α84F. Rabbi et al.理论计算机科学电子笔记295(2013)79输入:工作流程模型M结果:任务树λ(i) 使用词法分析创建标记;(ii) 使用定义2.1、2.2和2.3中提供的语法创建解析树λ,2.3(解析时,括号优先于运算符);(a) 为非叶节点的直接分支分配前提条件;(b) 将操作分配给叶节点(原子任务)。算法1.Text2TST:从工作流程模型的文本表达式构造TST单位为φ。例如,一个变量是可见的,并被添加到E中,尽管它不会出现在φ中,如果它忽略了一个运算符的先决条件,而运算符又忽略了φ中另一个变量的赋值。定义3.1(可见前提、动作、原子任务和操作者)动作α在α的受让变量中可见(参见定义。2.1)在E.一个原子(可补偿)任务τ是可见的,如果存在τ的任何可见的动作ατ。 操作符在其任何操作数中可见(可以是操作符或任务)是可见的。如果运算符可见,则运算符的前置条件可见。假设变量v1在E中,则动作v1 = 1成为可见动作,因为变量v1是动作的受让人;即,它出现在赋值操作的左侧。注意,如果v1出现在赋值操作的右侧,它将不会使操作可见,因为在这种情况下,操作将不会检查要验证的属性的真值切片算法通过消除E中不存在的所有节点和前提条件来构造简化的语法树λJ。下一个示例说明了算法例3.2(工作流切片)图图3示出了包含10个原子任务的工作流模型Mex我们希望验证的公式φ是:G((v1 == 1)→F(v2 == 1)),这意味着如果v1被设置为值1,则v2最终将被设置为值1。任务前提条件沿边缘显示,任务操作显示在任务下方工作流程的下部的文本表示如下:(({}任务2{ v1 ={ 1,2} } ·({v1 == 1}任务5{ v2 = 1} ×{ v1!= 1}任务6 { ·{ }任务9{ v6 = 1})。图4示出了Mex的TST。变量v1和v2可见,因为它们出现在φ中。任务任务2、任务5和任务3变得可见,因为可见变量v1和v2在它们的操作中显示为受指派者。然后,从这些任务到根节点的路径变得可见,并且所有的先决条件(v4!1,v4 == 1,v1== 1和v1!= 1)沿着这些路径将变得可见(用实线表示)。因为前提条件v4== 1和v4! 1变得可见,变量v4也变得可见。任务1变得可见,因为可见变量v4在其操作中显示为受让人。λex的其余部分将不可见(由虚线表示)。虽然可见变量v1出现在任务10操作的右侧,因为受让人变量V6不可见,则动作将不可见。F. Rabbi et al.理论计算机科学电子笔记295(2013)7985×输入:TSTλ和LTL公式φ结果:还原TSTλJ1E←;对于每个变量v∈φdo/* 添加LTL公式中的变量 */2E←E{v};3size←0;而大小E.大小4size←E.size;对于每个叶节点η∈λdo如果αη是可见的,则6E<$E <${η,αη}<$αη.variables;ηcurr<$η.parentNode;/* 递归添加所有祖先 */7当ηcurr不是根时,8E←E{ηcurr};/*带 条件的四个运算符 */9如果ηcurr为×或或+,则10ηl<$ηcurr.lef tChild;ηr <$ηcurr.rightChild;/* 添加所有分支条件 */11E<$E<${ηl,ηr}ηl.variablesηr.variables;12ηcurr←ηcurr.parentNode;/* 通过从λ*中消除不可见 元素来构造简化的语法树λJ/13λJ←λ;对于每个节点η∈λJ,14如果η∈/E,则15η←NIL;算法2. 分层算法v4!=1任务_3v1 = 2任务_7v6 = 2任务_1v4 ={1,2,3}v4 == 1X任务_4任务_8v3 = 2 v5 = 2v1 == 1任务_5Task_10任务结束v6 = v1 + 3v2 = 1任务_2v1 ={1,2}v1!=任务_9v6 = 1XXXvv任务_6v3 = 1图三. A sample work campaignMex86F. Rabbi et al.理论计算机科学电子笔记295(2013)79··v4 ={1,2,3}v4!= 1v4 ==exexexexexv4!=1任务_3v1 = 2任务_1v4 ={1,2,3}v4 == 1X任务结束v1 == 1任务_5v2 = 1任务_2v1 ={1,2}v1!=XXXvv·任务_1任务_2v1 ={1,2}1··任务_3Xv1 == 1任务_5v1 = 2 v2 = 1图四、本文给出了λex的语法树,并从图1中的Mex中导出3图五、约化功M ′从图中的工作流程Mex。3约化功WMJ如图5所示。 MJ并发任务但将为φ提供相同的验证结果(参见口吃等价物的证明(见第3.3节)。 在MJ中公式φ不成立;其中一个计数器,示例是以下任务执行顺序:(任务2→任务1→任务3→任务9→任务结束)。该计数器示例显示变量v1在任务Task 2中被设置为值1,并且在任务Task 3中被重置为另一个值2。为在这种情况下,公式G((v1 == 1)→F(v2 == 1))在MJ中不成立和因此不在Mex中。切片算法的复杂度在最好的情况下是O(n),其中n是原子任务的数量;这发生在所有任务都不可见时。 在这种情况下,算法对每个任务检查一次,然后停止搜索。最坏情况的复杂度是O(n2log n);这发生在算法在每次迭代中发现一个新的可见元素时。3.3口吃等价性的证明本节给出了工作流模型M和切片模型MJw.r.t.的口吃等价性的证明。LTL公式φ。我们采用了[4]中口吃等价的定义,使用了工作流模型生成的路径,v1!= 1v·F. Rabbi et al.理论计算机科学电子笔记295(2013)79870230J00J0其中每个状态由一个任务的执行产生,并且每个转换表示这样的执行。设V是系统变量的集合,其中变量的范围在有限集合D上,有时称为解释的域或论域V的赋值是将值d∈D与每个变量v∈V相关联的函数。AVP是一组原子赋值命题,其中每个命题通常具有v = d的形式。注意AVP是原子命题AP的子集。标号函数L:S→2AVP返回子集L(s)<$AVP,它在s∈S中为真。此外,可见标记函数Lφ为每个s返回其变量出现在φ中的子集Lφ(s)<$L(s)。定义3.3(可见标签函数)设φ是LTL公式,Vφ是φ中出现的变量集;状态s的可见标签函数Lφ(s)定义为Lφ(s)={p |var(p)∈ Vφ},其中p是L(s)中的命题,var(p)返回命题p的变量。我们现在定义路径和工作流模型的口吃等价性定义3.4(路径的断续等价两条有限路径π=(s0→S2 →s3... )和πJ=(SJ→SJ→SJ. )是口吃等价物w.r.t. 一个LTL公式φ,写作πφ πJ,如果有两个正整数序列0 = i0小时Prop3是的12801374488920.0397.9251323543153290.31931Prop4是的12793484188894.5396.1213254702140215.01854Prop5是的13479230.19.7202233451125804.11803Prop 2如果患者感到痛苦,则必须在护理团队中分配一名社会工作者。LTL:G((苦恼==1)→F(社会工作者==1))Prop 3如果患者的PPS为50%或更低,则必须将其转移到医院。LTL:G((pps≤50)→F((位置==2))Prop 4如果患者的优先级为3或更低,则必须将其转移到医院。LTL:G((患者水平≤3)→ F((位置== 2))Prop 5如果发现患者的活动能力发生变化,则LTL:G((移动性变化==1)→F(确认物理治疗师==1))在ACEnet(www.example.com)的Mahone2集群上用64个CPU和3GB存储器(每个CPU)执行所有实验www.ace-net.ca其结果示于表2。使用WS(工作流切片)+POR(部分)减少时间和内存与单独使用POR相比,降低了阶数。这些(和更大的)实验结果的更多细节可以在[16]中找到。我们还对不同类型的工作流进行了一般性能比较这些实验是使用DiVinE2.4在具有3GB内存的单个CPU上完成的考虑了只包含X的工作流、只包含X的工作流和只包含X的工作流对于operator,我们验证的LTL属性是两个任务,例如任务1和任务2,是否可以并发发生(即,G(任务1激活&&!任务2活动))。表3显示了对于不同数量的并发任务,使用WS和POR进行验证的转换数量。注意,我们已经通过矛盾证明了这个属性,所以切片算法排除除可见任务之外的所有任务。因此,在结果中,WS + POR中的状态数保持不变。使用不同数量的任务测试了带有×的工作流程,并确定任务1是否和任务2是互斥的(在LTL−X中,G(任务1活动→F(!任务2激活)|| G(Task 2 active → F(!任务1活动)。 测试了带有操作员接口的使用各种数量的任务,并且确定连接任务是否是最终可达的(在LTL-X中,G F(连接运算符活动))。从这些实验F. Rabbi et al.理论计算机科学电子笔记295(2013)7991表3(AND)、×(XOR)和情况任务加速循环PORWS + POR国时间(秒)国时间(秒)(AND)5是的107<115<110是的4396<115<115是的48784315<1×(异或)5没有27<124<110没有37<129<115没有47<134<1中文(简体)5没有99<11025<110没有2019731025<1结果我们可以看到切片的有效性;在有许多任务的情况下,它变得特别重要。5相关工作程序切片[21]是一种研究得很好的技术。其基本思想是抽象出不影响“兴趣点”的变量和语句程序切片可以应用于调试、测试、软件维护和形式化验证。Hatterygal等人[7]使用LTL公式中的原始命题提取切片标准,更重要的是,定义并形式化证明了程序切片的正确性Sloane和Holdsworth [20]提出了广义切片,它处理不同的切片,输入各种软件实体和构造。更重要的是,W.R.T.我们工作的相关性),他们使用程序语法树作为切片算法的载体。不幸的是,他们没有将正式核查纳入其框架。Millett和Teitelbaum [14]为Promela(模型检查器SPIN的输入语言)提出了Barbuti等人[2]从模型检验的观点出发,提出了一个一般的理论结果,证明了一个过渡系统模型与基于他们提出的称为选择μ演算的时态逻辑中所表示的公式的简化模型之间的等价性。所有这些工作都有力地表明,切片可以应用于不同抽象层次的建模语言。切片技术已被应用于Petri网。 Evangelista等人[5]至今着色Petri网(CPN)的一种约简技术。这种技术只保留了网络的活性,并且只保留了那些没有观察到网络的简化转换的LTL公式。 Rakow [18]提出了一种Petri网切片算法,并应用于它的LTL公式的验证;在文件中的案例研究是基于一个小的教科书工作流程的例子。我们注意到,CWML可以被视为CPN的抽象。我们需要两个不同的CPN,一个用于原子不可补偿任务,另一个用于可补偿任务[17],作为两个基本构建块并为每个复合任务建立了更复杂的Petri网。这种类型的抽象是需要的,因为现实世界的工作流通常是复杂的,它们的Petri网(包括CPN)模型很容易增长到太大而无法管理。有几个作品减少了工作流程模型的大小。 永利公司al. [23]提出YAWL[22]工作流的缩减规则,包括取消区域和OR连接,以减少工作流的大小,同时保留其基本功能。92F. Rabbi et al.理论计算机科学电子笔记295(2013)79公式w.r.t. 一个特殊的分析问题。 在那里,作者只关注可达性分析,而我们的切片方法适用于任何LTL−X公式。Awad等人[1]提出了BPMN图的约简过程,但缺乏对模型等价性的正式研究。ADEPT2 [19]工作流程可以使用SeaFlows合规检查器[10]进行验证[10]作者讨论数据抽象技术。由于切片和数据抽象相结合是这一领域的常见做法,我们希望他们的技术和我们的切片算法能够很好地相互补充。6结论和今后的工作提出了一种模型切片算法。 我们证明了原始模型和由算法生成的约简模型的口吃等价性。 这项技术已被纳入NOVA工作流程框架。我们的实验表明,该技术大大减少了验证的内存量和时间,使可补偿系统的真实世界模型的验证成为可能。我们希望CWML到其他模型检查器的转换是简单的。一旦开发出其他自动化翻译方法,其他模型检查器就可以用来验证大型工作流程模型。在未来,我们将在模型切片算法中考虑时间[13],因为医疗保健等安全关键系统中的许多规范都是时间敏感的。在[7]中,作者定义了控制依赖性,该依赖性可用于我们的方法中,通过预处理从模型中识别无限循环在未来,我们将加强我们的工作与非结构化的工作流程模型与无限数量的状态。确认这项研究得到了加拿大自然科学和工程研究委员会、大西洋计算卓越网络(ACEnet)博士后研究奖学金和大西洋加拿大机会局的支持。计算设施由ACEnet提供。引用[1] Awad,A., G. Decker和M. Weske,使用BPMN-Q和时态的逻辑,在:BPM 2008:第六届国际会议业务流程管理,计算机科学讲义5240(2008),页.326-341[2] 巴尔布蒂河,N. D. Francesco,A.Santone和G.Vaglini,选择μ演算和基于公式转换系统的等价性,计算机与系统科学杂志59(1999),pp。 537 - 556[3] B ARNAT , J. , L.B rim , M.Ces kandP.R oRuckai , DiVinE : ParallelDistributdModelCecker( Tolpaper ) , in : Parallel and Distributed Methods in Veri fication and High PerformanceComputational Systems Biology(HiBi/PDMC 2010)(2010),pp. 四比七[4] Clarke,E.M.,O. Grumberg和D.A. Peled,F. Rabbi et al.理论计算机科学电子笔记295(2013)7993[5] Evangelista,S.,S.哈达德和J. - F. Pradat-Peyre,Syntactic Colored Petri Nets Reductions,in:ATVA 2005:第三届国际自动化技术验证和分析研讨会,计算机科学讲义3707(2005),页。202-216[6] Ferris,F. D、H. M. Balfour,K. Bowen,J. Farley,M.哈德威克角Lamontagne,M. Lundy,A.Syme和P.J. West,《临终关怀姑息治疗指南模型》(2002)。[7] Hatterygal,J.,M. B. Dwyer和H. Zheng,Slicing Software for Model Construction,Higher Orderand Symbolic Computation13(2000),pp. 315-353[8] IBM、Bea、Microsoft、SAP和IBM,[9] Ip,C.N. 和D.L. Dill,通过对称更好地验证,形式方法系统设计9(1996),pp. 41比75[10] Knuplesch,D.,L. T. Ly,S.Rinderle-Ma,H.Pfeifer和P.Dadam,关于实现数据感知合规性检查业务流程模型,在:ER 2010:第29届概念建模国际会议,计算机科学讲义6412(2010年),页。332-346[11]李杰,H. Zhu,G.蒲和贺俊,一种可补偿交易的形式化模型,载于:ICECCS 2007:第12届 IEEE国际工程复杂计算机系统会议(2007),第100页。六十四比七十三[12] Louden,K. C.的方法,“Compiler Construction: Principles and Practice,” Course Technology,[13] Mashiyat,A.美国,F. 拉比和W。 MacCaull,建模和定时补偿工作流程2011年FMICS会议记录:第16届工业关键系统正式方法国际研讨会,计算机科学讲义6959(2011),第16页。244-259.[14] 米利特湖I.和T. 李文生,李文生,李文生,等.基于分层的网络协议分析方法.北京:计算机科学出版社,1998. 75比83[15] Peled,D.,十年的偏序约简,在:CAV 1998:第10届计算机辅助验证,计算机科学讲义1427(1998),页。17-28.[16] 拉比,F.,“Design, Development and Verification of a Compensable Workflow Modeling Language,”Master’s 数学,Stats. 和CS,StFX大学,加拿大(2011年)。[17] 拉比,F.,H. Wang和W. MacCaull,可补偿工作流网,在:ICFEM 2010会议录:第12届正式工程方法国际会议,计算机科学讲义第6447(2010)号来文,第100页。122-137[18] Rakow,A.,切片Petri网与应用到工作流验证,在:SOFSEM 2008:第34届会议当前趋势的理论和实践的计算机科学,讲义在计算机科学4910(2008),页。436-447[19] Reichert,M.,S. Rinderle,U. Kreher,H. Acker,M.林文辉,“新一代制程管理技术”,载于第四海德堡创新论坛(2007)。[20] Sloane,A. M. J. Holdsworth,Beyond Traditional Program Slicing,ISSTA 1996:InternationalSymposium on Software Testing and Analysis(1996),pp. 180-186[21] 提 示 , F. , A Survey of Program
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- 图书馆管理系统数据库设计与功能详解
- ***物流有限公司仓储配送业务SOP详解
- 机械专业实习经验与学习收获
- 阎良区生活垃圾卫生填埋场施工与运营管理详解
- 濮阳市生活垃圾无害化处理工程施工组织设计详解
- MATLAB均匀平面波仿真课程设计指南
- 北京市地铁9号线技术规格与设备详情
- 西门子PLC在中央空调自动控制系统的应用
- PLC驱动的电梯控制系统发展历程与未来趋势
- 外墙维修工程政府采购项目施工方案概述
- 项目方案委员会会议全程指南与文件清单
- Dreamweaver实战:创建简单网页与站点管理
- 国内升学与就业政策及信息搜集指南
- 国资公司2020上半年创新发展与资产管理工作总结
- 项目管理:目标控制与各方角色分工详解
- 构建项目管理体系:提升组织绩效的关键
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功