论文研究 基于二次分配问题的混合蚁群算法.pdf

UML已经是软件建模方面的标准语言，UML Statechart描述了系统在其生命周期中的动态行为。随着系统规模的扩大和复杂度的提高，Statechart往往包含设计者所未预料到的隐患，通过模型检查来对Statechart进行穷举检验就成为一个重要课题，首先给出了含层次、并发Statechart的语义；随后提出了对Statechart进行模型检查的一种新方法，并且已经编写软件SC2Spin实现此方法，该方法使用了提出的Statechart山脉算法和迁移提取法，可以将一个Statechart自动转化为Spin的输入语言Promela，从而验证Statechart的死锁、活锁等错误和时序逻辑公式。郭伟,缪力,张大方,等:基于Spin的UML状态图模型检查的设计与实现2008,44(10)45E(D)=1,c(H)=0。o(F)=A,o(C)=B。状态F到状态G的迁移中,事件集E=k1},条件集C′=k≥5},动作集A′={u=1}{A,B,D,G}、A,E,F都是格局,而{A,B,G,F则不是格局。如图2所function3(s )示,2的最小公共祖先lca(t2)=A,1l的出发状态是 Source(t1)=-w(SH,目的状态是aret(t1)=D。if(d! =lcat))(for(i in 8(d))(A 1 Endif(e(i)!=8(s))Q. add(i)InitialA1 InitialBl_ ofunction3(d);仅当两个迁移所退出的状态集的交集不为空时:exi(t)∩exi(t')≠,迁移间发生冲突,此时,UML规定出发状态层次高的迁移有较高的优先级:如果 source(t)∈p+( source(t')),则选择迁移t。如图2中迁移t2和4发生冲突时,2优先级高。End如图2所示,ener(t1)=D,B,A∪F},exit(tl)={H,ext(t2)=图1包含并发和层次的 Statechart)(B)=B, C, D, Bl_End), enter(t3 )=(0, exit(t3 )=(H), enter(14)=UML Statechart的执行语义是通过RTC( Run to Comple-),emi(14)={B,C,D,B1Enl)。如图3所示, enter(t3)={H,ion)定义的:每个 Statechart对象都有:(1)一个事件队列充当,ex(13)=(E,C,ener(14)={F,BUGU(,ex(14)=)事件池,保持到达的事件,直到它们被一一派遣出队列;(2)种事件派遣机制,在事件队列中选择事件并丛队列中移除。个 Statechart一次只能从事件队列中派遣出一个事件,并且必须等到上一个事件完全处理完毕后才能派遣新事件。从一个事Ht1件被派遣,直到 Statechart到达下一个格局,就是 Statechart的13一个Sep,它是状态机对一个事件的处理方式,连接了两个格局,如果一个被派遣的事件不能使任何迁移发生并且不属于当图2对应于图1的 Statechart山脉算法图前格局的延迟事件,则被丢弃。一个事件在并发状态格局中可能激发多个迁移,但是每个并发子状态只能激发一个迁移,此3 Statechart山脉算法后,如果这个格局在不需要任何事件的条件下就可以继续执行本文提出的 Statechart山脉算法,在传统 Statechart基础下面的Sp,那么这个格局就是一个瞬时格局,或者称不稳定上,将除最底层外的所有复合状态表示为立方体,好像山脉隆格局, statechart将继续执行直到稳定格局为止。所以两个稳定起;将所有 basic状态表示为平行四边形,好像山脉上一片空格局间可能存在多个瞬时格局。地;状态间的迁移便可以归纳为4类:平地走、上山、下山和先当一个迁移t被激发时,用ext(t)来表示迁移t的退出状下山再上山。从图2中可以形象地看出,复合状态A中的复合态集,用 enter(t)表示迁移t的进入状态集:状态B,像山脉一样隆起,而 basic状态F和G则像一块空地。xt(t)p(s),其中s∈p(lca(t)∧ sources)∈p(s)复合状态B中的 basic状态C和D同样也像空地。于是迁移可ener()=0UP∪Q,用三段伪代码计算三个集合C2Spin以分为4类,第1类是“上山”,如图2中的t迁移,直接指向已经实现这三个函数), unction1.(0递归计算伴随mg()同时D状态就上了B状态这座山;第2类是“平地走”,如图2中的激活的所有父亲状态与get(t)本身的合集nin2()通递归状态C到D的迁移,F到G的迁移;第3类是“下山”,如图2计算伴随lgrt()同时激活的所有子状态集合mctm3()递中的状态D指向A1End的迁移,下了复合状态B这座山;第归计算伴随 function1(所产生父亲状态的开始状态集合。设4类是“先下山再上山”,如图3中的迁移3。当tet(t)和s=target(t)source(t)均为basc状态时,在下山和平地走的情况下,进入状furnotion(S)态集可以简化为 enter(t)= target(t);在平地走和上山和的情况O. add(s):下,退出状态集可以简化为exit(t)= source(t)。if(o(s) =lca(t)(1)平地走时function(o(s如果 target(t)为 basic状态,那么 enter(t)= targe(t);如果 target(t)为复合状态,那么 enter(t)=oret(t) Funcfunction2(s)tion(target(t))If(u(s)==ANDIlA(S==OR )(如果 source(t)为 basic状态,那么exi(t)= source(t);P. add(d):如果 source(t)为复合状态,exi(t)=Pp( source(t));function2( d)(2)下山时, enter(t)如同平地走:exi(t)→p(s),其中s∈p(la(t)) Asource(t)∈p(s);462008,44(10)Computer Engineering and Applications计算机工程与应用(3)上山时,exi()如果平地走表1描述 Statechart的xml文件结构如果 target(t)为 basic状态,那么实例xm源代码描述enter(t)=functionItarget(t))Ufunction3(target(t))状态名称,此名称必须唯如果 target(t)为复合状态,那么isinitialy"false""false"enter(t)=functionI( target(t ))Ufunction2(target(L))是否为终止状态"false"是否为最终终止状态function 3(target(t))"false"是否为复合状态或并发状态(4)先下山再上山时, enter(t)的情况同上山,exi(t)的情况 parentnode>"inga"< parentnode直接父亲状态名称同下山。迁移列表结构为 event:事件guard=kuai[1]&&kuai[O]守护条件BI-EndEndaction=" kuai[Ok-false; kuai[fAlse; A count+"迁移所引发的动作D迁移所引发的事件迁移的目的节点从内而外依次列出C-EndF-Endgotoout="fal是否跳出其父状态willinactive="A-think迁移执行时,离开的最外层状态●B2-End图3 Statechart山脉算法图atomIc(所引发的事件、动作::(迁移2发生的条件)→>4 Spin/promelaspin( Simple Promela Interpreter)是由美国贝尔实验室开atomic所引发的事件、动作。}发的,2002年荣获ACM的“ Software System Award”’。选择spin(迁移n发生的条件)->作为验证工具主要是因为Spin应用∫很多高效的状态空间搜atomic(所引发的事件、动作。}索技术,大大提高了搜索效率,spin的建模语言 Promela拥有基本数据类型和各种语言结构,这使得 Promela语言的可读性临时变量归零。和表达能力都非常强,它的建模方式是以进程为单位,进程异步交互运行。进程的基本要素包括赋值语句、条件语句、通讯语:(迁移1是否发生)->句、非确定性选择和循环语句。Spin可以随机模拟系统的一条atomic(设置迁移的目的状态为激活状态}执行路径,也可以实时自行选择执行路径;spin所验证的L(迁移2是否发生)->公式如<>P的形式,其中P定义为一个性质,如A1==5,表示atomic{设置迁移的目的状态为激活状态永远( forever)”或“总是( always)”,<>表示“最终( eventually)”<>P的意义是A1的值终将为5。同时定义了“直到( until)”(迁移n是否发生)->P∪Q意为性质P为真直到性质Q为真。检查到性质不符合atomic(设置迁移的目的状态为激活状态时,即得到反例时,spin可以给出这个反例的执行路径,以便研究者精确发现问题所在。临时变量归零5迁移提取法测试是否应该派遣下一个事件,是则派遣,否则返回。本文在 Statechart转化为 Promela方面提出了迁移提取事件处理队列,如果没有迁移可以发生,即已经结束了法,概括的说,首先用一个xm文件精确表示 Statechart,然后一个Step,则下一个事件被派遣提取该xml文件中所有表示迁移的段到一个 Promela的do循环中,再提取xml文件中所有事件到do循环的else语言中,实Deadlock: printf(" Deadlock");没有事件可以被派遣,而程序不可继续运行,即死锁时则指向这条语句。现一个先进先出(FIFO)的队列实现事件的处理,总体来看,实TheEnd:skip;此语句用于结束程序。当指向最终终止节点的迁现R℃语义。为了自动完成迁移提取法,作者编写了软件移发生时运行SC2spin,使用者可以首先用它来画 Statechart,然后就可以直接转化为一个xml文件和一个 Promela文件。转化过程完全不需人手工干预,在进入spin验证时,仅需要在 Promela文件前加6实验入 Statechart中所有的变量的定义并初始化,如 int a count=0。图4是一个哲学家就餐问题的 Statechart,采取一次拿起描述这种 Statechart的xml文件由本文作者定义,基本结个筷子的方法,称其为方法1。这里仅考虑两个哲学家的情构如表1所示。况,拿哲学家A为例,A- think表示哲学家A在思考状态,A使用迁移提取法所生成的 Promela代码结构为:ready表示拿到一支筷子的状态,整数A-have的值表示拿起所有变量定义;了几支筷了, A-eaLx表示拿起两支筷了的状态,即进食状态,active proctype ourtypeA-end表示停止进食,处于结束状态。哲学家A进食5次后,即do:(迁移1发生的条件)-A_ count=5时,到达A-end状态;不满5次,回到A- think状郭伟,缪力,张大方,等:基于Spin的UML状态图模型检查的设计与实现2008,44(10)4态。当两位哲学家航餐次数都到达5次后,并发状态lnga结東,即整个程序停止。两支筷子用ka2尔数组表示,kua0-=tme表示此筷子在桌上,kui[0-fle表示此筷子已经被哲学bingkuai[O]=true; kuai[l]=true家拿起。这样是香可以避免死锁呢?kuai[l]=&&kuai[Olkuai[]=false; kuai[l]falseA-think●kuaiA-readykuaill]false; A_have++;A_count++a count<5A countkuai[o=true; kuai=trukuai[o]=false; A_have++-eatl] kuai[O=true; kuai[ll=trueB count==sA-thinkcounteskuai[OFtrue; kuai[l]=truekuai[O]=true; kuai[1]=true; A_have=0kuai l&&kuai[oA count<5kuai[OFfals; kuai[ 1]=false; B_count++kuai[l]kuai[O=true; kuai[ l]=true; A_have=0-think-eatkuai[l]=false; A have++A-eat2 A_count==5A6-ready2lkuai[o]=true; kuai[l ]=trueBcount< skuai[O]kuai[o]=true; kuai[l=truekuai false: A have++: A count++kuai[l]kuai[l]=false; B_have++; B_count++kuai[ol=false; B_ have++B count==5B-eatlk kuai[O]=true; kuai[ltrue图62位哲学家采用方法2就餐的 Statechartkuai[oftrue; kuai[ l=true; B_have=07结论B countAcon=5,即 a count能否终将等于件,但是并没有覆盖 UML Statechart的全部语义,如历史伪状5,如果发生死锁的话,这个性质不成立,验证结果如图5所示态、延迟事件等。这都有待于下一步的工作为 not valid,即会发生死锁。a Linear Time Temporal LooX参考文献:[1] Object Management Group. version 2.1.1 Unified Modeling LanOperators:0<>U->and or notsymbol DeTnltonsguage: Superstructure[S].2007A #define pA count==5[2] Clarke E M Jr, Grumberg 0, Peled D A Model checking[M]. 4th edCambridge, Massachusetts MIT Press, 2002erification Result: not valid: Run Verification3] Holzmann G J.The spin model checker: primer and reference man图5Spin的验证结果截图ual M-S.]: Addison Wesley, 2003换一种拿筷子的方式,称其为方法2,如图6所示,哲学家4MOCES:ModelCheckinGStatecharts[cp/ol].http:/www.informatikA只有在旁边的两个筷子kmi0和km[都为tre时,才同时uni-kiel. de/inf/de roever/research. html拿起这两个筷子, A count自增,到达A-eat状态。到达A-eat5]MikE, Lakhnech y,seM,eta. Implementing statecharts in状态后,如果就餐次数小于5,则放下筷子,进入A- think状态PROMELA/SPIN[C]/Proceedings of the 2nd IEEE Workshop on如果就餐次数到达5次,则进入结束状态A-end。当两位哲学Industrial-Strength Formal Specification Techniques, IEEE Computer Society, October 21-23, 1998: 90-101家就餐次数都到达5次后,并发状态 bingfa结束,进入End状态,整个程序停。这里采用哲学家必须同时拿起两个筷子的6 Latella d,Majk, Massink M. Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model方法,是否避免了死锁呢?checker[J] Formal Aspects of Computing, 1999, 11(6): 637-664验证LL公式<>4 count=5,验证结果为 valid,那么图 Latella d, Majik1, Massink m. Towardsa formal operational seman-6的办法已经避免了死锁。tics of UML statechart diagrams[ C]/Proc FMOODS99, IFIPTC6/现在提岀假设:n个哲学家就餐问题,至少有一个哲学家WG6.1. Third International Conference on Formal Methods for采用方法2,就可以避免死锁。Open Object-Based Distributed Systems, Florence, Italy, February本文考虑了3位哲学家的情况,哲学家A、B采用方法115-18,1999哲学家C采用方法2,同样用 X count表示吃饭次数,验证LTL[8] Paltor I, Lilius J. uml: a tool for verifying UML models[C]/Proc of公式<> A count==5和<> C count=5,验证结果均为 valid说the 14th ieee International Conference on automated softwaare明假设成立Engineering, ASE 99, IEEE, 1999