基于自动机理论的UML活动图模型检验方法

基于自动机理论的UML活动图模型检验方法 基于自动机理论的UML活动图模型检验方 法 第19卷第22期 2007年11月 系统仿真◎ JournalofSystemSimulation V0119NO.22 NOV.20o7 基于自动机理论的UML活动图模型检验方法 王聪,王智学 (1.解放军理工大学通信 工程 路基工程安全技术交底工程项目施工成本控制工程量增项单年度零星工程技术标正投影法基本原理 学院,江苏南京210~7;2.解放军理工大学指挥自动化学院,江苏南京210~7) 摘要:UML活动图被认为是最合适的软件过程描述语言,研究UML活动图的模型检验方法是很 有必要的.提出一种基于自动机理论的UML活动图的模型检验方法.该方法给出UML活动图的形 式语义,通过计算RTC.STEP,得到LTS,并将LTS映射到Btichi自动机,用L11IJ表示系统性质, 并将u1IJ公式转换为相应的Bi.ichi自动机,用基于自动机理论的模型检验方法捡_罩套UML活动图. 关键词:UML活动图;形式语义;模型检验;Btichi自动机 中图分类号:TP311.5文献标识码:A文章编号:1004—731X(2007)22—53l1—04 AutomatonTheory-basedModelCheckingMethodforUMLActivityDiagram WANGCong,WANGZhi-xue (1.InstituteofCommunicationsEngineering,PLAUniversityofScienceandTechnology,N anjing210007,China; 2InstituteofCommandAutomation,PLAUniversityofScienceandTechnology,Nanjing21 0007,China) Abstract:UMLactivitydiagramiSregardedasthemostsuitable1anguagetodescribingtheS Oftwareprocess.ItiSworthto researchingtheapproachofmodelcheckingUMLactivitydiagram.Anapproachofmodelch eckingUMLactivitydiagram wasprovided.formalsemanticsofUMLactivitydiagramwasgiven.LTSfLabeledTransitio nSystem)wasdeducedby computingtheRTC-STEP.Andthenthe 【ScouldbemappedtoaBfichiautomaton.rhesystempropertiescouldbe describedbyLTL.LTLformulacouldbetranslatedtoaBrichiautomaton.LactivitydiagramC OUldbecheckedv nMtomntontheory—basedmodelcheckingmethod Kevwords:UMLactivitydiagram;f0rma】semantics;mode1checking;Brichiautomaton 引言 UML(UnitedModelingLanguage)是对象管理组织 OMG(ObjectManagementGroup)第三代面向对象建模语言 】 .它定义了多种图元,从不同视角和层次描述了系统的静 态结构和动态特性.它是一种定义良好,易于表达,功能强 大,且普遍适用的建模语言.广泛适用于各种应用领域,并 己得到工业界的广泛支持.许多大型系统均采用UML作为 需求描述语言进行分析和 设计 领导形象设计圆作业设计ao工艺污水处理厂设计附属工程施工组织设计清扫机器人结构设计 .UML活动图是一种特殊形 式的状态机,用于对工作流程建模,在UML所提供的5种 可用于描述系统动态行为的图中,活动图被认为最适合描述 软件过程模型【2.】.活动图强调从活动到活动的控制流. 模型检验(modelingchecking)是一种形式化验证技术. 模型检验的研究始于八十年代初,当时Clark,Emerson等 人提出了用于描述并发系统性质的CTL(ComputationTree Logic)逻辑,设计了检验有穷状态系统是否满足给定CTL公 式的算法,并实现了一个原型系统.这一工作为对并发系统 的性质自动验证开辟了一条新的途径,成为近二十年来计算 机科学基础研究的一个热点.模型检验的基本思想是用状态 迁移系统()表示系统的行为,用时序逻辑公式(,)描述 收藕日期:200609—18肇回日期:2006—12—05 基金项日l总装备部十五预研项目(413060103) 作者简介:王聪(1975一),男,安徽人,博士,研究方向为指挥自动化系统 理论,软件工程;王智学(1961.),教授,博导. 系统的性质.这样"系统是否具有所期望的性质"就转化为数 学问题"状态迁移系统是否是公式F的一个模型?",用公 式表示为S'F?.近年来出现的UML活动图的模型检验方 法基本上都是将活动图作为一种特殊的状态机,而直接套用 状态机的模型检验方法【3】.这样忽略了活动图的特殊性, 使得活动图的模型检验不直观,不自然.实际上,在UML 所提供的5种可用于描述系统动态行为的图中,活动图被认 为是最合适的软件过程模型描述语言【2],所以研究UML活 动图的模型检验方法还是很有必要的. 本文提出基于自动机理论的活动图模型检验方法.检验 的步骤为:1,建立系统自动机A;2,将系统的性质用 LTL(LinearTemporalLogic)公式妒描述,并为性质妒的否定 命题建立BOchi自动机A;3,计算两者的乘积AxA; 4,检查该乘积自动机所能接受的语言是否为空.下面我们 首先给出活动图的形式语义,通过该语义得到LTS(Iabelled TranstionSystem),并最终由LTS得到系统自动机A. 1UML活动图的形式语义 1.1形式化语法 UML活动图是一个有向图,由节点和有向边构成.UML 活动图的基本元素有状态,变迁和动作.状态表示过程中所 处的各种状态,而不是普通对象的状态,它不仅包括状态名, 还包括进入动作(entryaction),离开动作(exitaction)和 内部变迁等.变迁表示活动的流程或对事件做出的响应.动 ?53l1? 第l9卷第22期 2007年11月系统仿真 ,,0I_19No.22 Nov.2o07 作包括产生新事件,修改属性值和调用其他对象的操作. 1.1.1状态 UML活动图的状态分为动作状态(actionstate),活动 状态(activitystate)和伪状态.动作状态是原子的,不能被 分解,其执行过程不可中断;活动状态能够进一步分解为多 个活动状态;伪状态包括初始状态(init),分又(fork),汇 合(ioin),分支(branch),合并(merge)和终止状态(fina1). 设S表示非空的有限状态集,initial,fina1分别表示活 动图的初始状态和终止状态,则有initial?S,final?S. 定义1UML活动图的动作状态(Actionstate):动作状态 可表示为如下六元组, ActionState:::(n,entryAction,DoActivity, isDynamic,dynArgs,dynMu1), 其中n表示该状态的状态名j;entryAction,DoActivity分别 表示该状态的入口动作和活动;isDynamic一个布尔变量, 表示该状态是否可以并发执行;如果isDynamic=true,则 dynArgs表示状态每次执行时的参数集合:相应的dynMult 则表示状态并发执行的次数. 定义2UML活动图的活动状态(Activitystate):活动状 态可表示为, ActivityState::=(n,entryAction,DoActivity,exitAction,D,Z, out,event,isDynamic,dynArgs,dynMult), 其中n表示该状态的状态名;;entryAction,DoActivity, exitAction分别表示入口动作,活动和出口动作;D表示该状 态相关的子活动图;1表示该状态的当前活动状态;out表示 该状态的退出状态;event表示中断执行D的事件,event可 以为空;isDynamic一个布尔变量,表示该状态是否可以并发 执行;如果isDynamic=true,则dynArgs表示状态每次执行时 的参数集合;相应的dynMult则表示状态并发执行的次数. 1.1.2变迁 UML活动图的变迁包括如下元素:源状态,目标状态, 激发事件,布尔条件和动作.下面记激发事件,布尔条件和 动作的相应集合分别为Event,Guard和Action,若e?Event, c?Guard,日?Action,则L=e[c]/a为一个变迁标记,所 有的变迁标记集合记为Labs,用L表示变迁标记只有动作 的标记集,t表示变迁标记只有布尔条件的标记集,其中 厶Labs,LrLabs.则有如下变迁的定义. 定义3UML活动图的变迁可定义为:TcNames×2x (Eventsu)×Guards×Actions×2,对于(,x,e,g,as,Y)?T 有n?Names,x.y?S,e?Event,c?Guard,a?Action. 为方便起见,定义如下函数:Vt=(n,x,e,g,as,),)有: Names(t)=n,Source(t)=x,Event(t)=e,Guard(t)=g, Action(t)=as,Target(t,=Y. UML活动图的变迁关系分为简单变迁和复合变迁,简 单变迁是指变迁的源状态和目标状态都是动作状态或活动 状态等基本状态,复合变迁指由伪状态ioin,fork,branch 或merge连接的简单变迁族,它们存在多个源状态和多个目 标状态.Join将多个并发状态连接到ioin状态;fbrk将变迁 分割成多个并发的状态;branch将单个变迁划分成多个条件 的变迁分支,它必定有标记为else的分支. 设T={t,,t.,…,t)是非空的变迁集,xcS是非空的 状态集: 若#x=n2,则当t,,厶,…,?厶,L?Labs,?S 时,join(X,,,.,…,L,^,L)=s有定义,??{Ln),3s?X 使tl=(s,,join)?T,t=(join,L,)?T. 若#X=n?2,则当.,,…,?厶,L?Labs, s?S时,fork(s,L,,,,…,,L)=X有定义,Vi?{1,…,n}, 3s?X使t=(fork,L,.,s,)?T,t:(s,L,fork)?T. 若#X:n?2,则当t,L,,…,?,L?l_22bs,? 时,branch(s,,,t.,…,,L)=X有定义,Vf?{1,…,n}, 3s?X使=(branch,厶,s,)?T,t:(,L,branch)?T, 有且仅有一个关键字else?{t,,L:,…,}. UML活动图的连接子分为AND一连接子和OR-连接子, 其中join和fork是AND一连接子,branch是OR-连接子.设 join,fork,branch各自所连接的变迁构成集合 T=It,,t.…,t}(n?2),对应的复合变迁为CT.则由join, fork,branch连接的变迁满足: (1)如果连接子是branch,则存在n一1个变迁,设每个 变迁表示为CT=fCX.CLCY,且其中有且仅有一个变迁 2<in,t?T满足:CX=Source(ti),Event(CT)=Event(t,), Guard(CT)=True,CY:Target(tj),Action(C1")=Sequence [Action(t,);Action(t)】. (2)如果连接子是join,一定存在变迁CT:fCX. CL,Cy),其中cY=Target(t),Event(CT)=Event(t.), CX=USource(ti),Guard(CT)=Guard(t,,Action(CT)= lI—l Sequence[Concurrence[A];Action(t.)】,A=Action(tf),…, Action(t.一】); (3)如果连接子是f0rk,一定存在变迁CT=(CX,CLCr), 其中CX=Source(t),Event(CT)=Event(t),Gurad(CT)= Guard(t),CY=UTarget(t~),Action(CT)=Sequence 2SlSn 【Action(t1);Concurrence[A]】,A=Action(t2),…,Action(t), 其中Sequence[]和Concurrence[]分别表示动作的顺序关系和 并发关系. 1.2形式语义 1.2.1UML活动图的格局 在UML对象创建之初,初始状态是活跃的,所有活跃 状态构成活动图的当前格局,表示整个活动图的全局状态. 在活动图的执行过程中,当进入一个状态时,则该状态被激 活,如前所述,由于UML活动图中没有定义严格的层次关 ?5312? 第19卷第22期 2007年11月王聪,等:基于自动机理论的UML活动图模型检验方法 V1.19No.22 NOV..2(x】7 系,所以一个状态在同一时刻可能被激活多次,这样,活动 图当前的格局就不再是一个当前活跃状态的集合,而是活跃 状态的包(bag)【,则有下面的定义. 定义4:设UML活动图的当前状态为S,则S的格局 C(s)为满足以下条件的包(bag): S属于C(s); 如果C(s)包含OR一连接子A,则C(s)必定包含且仅包含 A的,个分支状态; 如果C(s)包含AND一连接子A,则C(s)必定包含A的所 有并发状态; c(s)为满足上述规则的有限包. 1.2.2UML活动图的操作语义 UML活动图操作语义可以用一个LTS来定义,包含通 过变迁相关联的一组状态集,采用标记变迁系统LTS来定义 操作语义,它是一组由变迁关系连接的状态集,变迁为 RTC—STEP(Run—To—CompletionStep). 定义5UML活动图的语义由M=(S,Label,_?,S.)?LTS 给出,M是一个Kripke结构,其中: s是当前格局; Label:S2,是标记集合,其中AP表示原子命题 的集合; S×S是变迁的集合; S是初始格局. 对于(J,)?_?,可以用—'来表示,称活动 out 图由当前格局S,在事件e,布尔条件c下,执行活动a,转 换到格局s,并产生新的事件集合out. 上面给出了活动图的形式语义,下面根据该语义给出生 成LTS的算法框架,算法如下文所示. procedureGenGIobalConfigO whiletruedo selectaeventfromeventqueue; computeaenabledstep; computeaRTC-STEP; takeastep; computetheneweventandaddittotheeventqueue; generatenewactivities; endwhile endproc 2系统性质的LTL描述 2.1IJTL的语法及语义 LTL由原子命题,逻辑连接符和模态算子组成.LTL的 逻辑连接符包括:_1,人,V.它的模态算子包括:X(Next), F(Finally),G(Globa1),U(Until),R(Release).给定 原子命题的集合AP,则LTL的语法定义如下: 如果P?AP,则P是一个LTL公式; 如果f和g是公式,则]厂,f^g,fvg,xf,Ff, Gf,fUg和fRg是公式. LrL的语义由Kripke结构M:(Label,_?,.)定义. 定义6路径(path):M=(Label,_?,)中的一条路 径是一个状态的无限的序列7l"=…,并且有 V(S,S…)?_?. 根据需要检验的活动图的性质,定义以下原子命题: in(s):其中S是系统状态,即in(s)表示SEC xopY:x是变量,Y可以是变量也可以是常量,op是 相关的逻辑关系,xopY为真时表示x和Y满足关系op: O(e):表示发生事件e. 2.2LTL公式到Biichi自动机的转换 将LTL公式转换为表示相同无穷状态的?一自动机,人 们已经做了很多工作,R.Gerth等给出了第一个高效的转换 算法,在他们的工作的基础上,人们相继提出了许多改进 算法】,其目的都是要在更短的时间内得到规模更小的?一 自动机. 下面本文给出算法的一般步骤,详细设计请参阅相关文 献【8—12】.要得到相应的自动机,需要做以下1作: Step1:将LTL公式转换成否定正规形式,即否定符号 只出现在命题之前,且模态算予只包含u,R,x种,其 转换规则如下: F三TrueU; G三FalseR; (_厂Ug)三(—]厂)R(--g),(_厂Rg)三(—]厂)u(g); 一 U厂三X1厂. Step2:分解公式,其规则如下: u=V(^u))R=^(vX(qRV2)) 直到所得到的公式是基本公式(elementaryformula)为 lf=.所谓基本公式是指公式为常量(True或者False),或者 是原子命题,或者是X,formula.将这些基本公式表达成析 取范式(DNF),称为的覆盖(cover),即:Akr&HVAj cover中的每一项标识自动机的一个状态(state),每项中的 原了命题以及它们的否命题构成状态的标志(1abe1).每项 中剩下的基本公式则组成项的nextpart,它是公式在下,个 状态中必须满足的.这样对每项的nextpart部分继续分解, 建立新的covers,直到不再产生新的nextpart为止. Step3:构造自动机:covers中的项构成自动机的状态; 的基本cover中的项构成自动机的初始状态;将每个状态 和它的nextpart状态连接起来构成自动机的转换关系;为每 个(pUlf,形式的子公式建立接收集. 2.3UML活动图的模型检验方法 根据前面给出的检验的步骤,再得到系统自动机和性质 自动机后,下面就是要得到两个自动机的乘积并判断该乘积 自动机所接受的语言是否为空,如果为空的话,则说明性质 ?5313? 第19卷第22期 2【x】7年11月系统仿真 Vbl_19No.22 Nov一2【x】7 是可以满足的.自动机判空的问题可以归结为:给定一个有 向图G,初始节点为s,接收节点集合为F,确定是否在F 中存在一个节点从可达且属于一个环路.文献【13】给出高 效算法.该算法的优点在于如果自动机非空,则可以得到自 动机所接受的语言,这样可以提供反例路径供性质不满足 时,调试系统用.完整的检验过程如图1所示. 图1系统验证过程 2.4举例 性质:行为不产生死锁.用LTL描述为:R:FG(in(fina1)). 计算过程如下: ~ (FG(in(fina1)) 甘~(F(FalseR(in(fina1)))) {一(7"PU((Fa&eR(in(.口,))))) 甘Fa&eR一(凡7PR(in(fina1))) 甘Fa&eR(TrueU~(in(fina1))) 生成Biichi自动机,如图2所示,其中P=in(fina1). 3结论 图2Bfichi自动机 本文全面,完整的给出了基于自动机理论的活动图模型 检验方法,该方法从自动机理论出发,首先将系统转化为 LTS系统,并将其转换为Btichi自动机:然后用岍描述系 统应具备的性质,并将性质的否定命题转换为相应的Biichi 自动机:最后在得到系统自动机与性质自动机乘积自动机的 基础上,判断该乘积自动机可接受的语言是否为空,如果为 空则说明系统满足所给出的性质,如果不满足,则给出反例 路径,进行调试,直到满足为止. 参考文献: [1]OMGOMGunifiedmodelinglanguagespecification(Version1.5)[R】 Needham:ObjectManagementGroup,Inc.,2003. [2]RumbaughJ,JacobsonI,BoochGTheUnifiedModelinglanguage ReferenceManual[M].Boston:Addison-Wesley,1999. [3]MikkE,LakhnechY,SiegelM,eta1.ImplementingStatechartsin PROMELMSPIN[c]//ProceedingsoftheWorkshopon Industrial—StrengthFormalSpecificationTechniques(wlgr'98). Washington,DC:IEEEComputerSociety,1998. [4]LiliusJ.PaltorIP.vUML:atoolforverifyingUMLmodels[c]//Hall R,TyuguE.eds.Proceedingsofthe14ttiIEEEInternational ConferenceonAutomatedSoftwareEngineering.Washington,DC: IEEEComputerSociety.1999:255—258. [5]GnesiS,LatellaD.ModelcheckingUMLstatechartsdiagramsusing JACK【C]//Proceedingsofthe4thIEEEInternationalSymposiumon High—AssuranceSystemsEngineering.Washington,DC:IEEE ComputerSociety,1999:46—55. [6]EshuisR,WieringaRAformalsemanticsforUMLactivitydiagrams [R].TechnicalReportTR?CTIT-01—04.Hengelo,Netherlands: UniversityofTwente,2001. [7]GerthR,PeledD,VardiMY,eta1.Simpleon—the—flyautomatic verificationoflineartemporallogic[c]//DembinskiP.SredniawaM, edsProceedingsofthe15thInternationalSymposiumonProtocol SpecificationTestingandVerification.Boston:KluwerAcademic Publishers,1995:3—18. [8]DanieleM,GiunchigliaVardiM.Improvedautomatagenerationfor lineartemporallogic[CJ//NHalbwachs,DPeled,editors,Proc.of ComputerAidedVerication:1lthInt.Conf.,CAV99,Trento,Italy: LNCS1633,1999:249—260. [9]SomenziBloemR.EfficientBuechiautomatafromUFormulae [c]//Proc.Ofthe12thInternationalconferenceonComputerAided Verification(CAV2000)Chicago,USA:Springer,LNCS1855.2000: 247—263. [10]GastinP,OddouxD.FastL1LtoBuechiAutomataTranslation[C]// Proc.ofthe13thInternationalConferenceonComputerAided Verification(CAV2001),Paris,France:Springer,LNCS2102.July 2【x】1:53.65. [11]GiannakopoulouD,LerdaEEfficienttranslationofUformulaeinto Biichiautomata[R].RIACS,TechnicalReport,01.29.RIACS:RIACS 2001 [12]WolperP_ConstructingAutomatafromTemporalLogicFormulas:A Tutorial[c]//ProcoftheFMPA2000summerschoo1.Nijmegen,the Netherlands:Springer-Verlag,2000:261—277. [13]CourcoubetisC,VardiM,WolperP,eta1.Memo~一Efficient algorithmsfortheverificationoftemporalpmpe~es[C]//Formal MethodsinSystemDesign.Hingham,MA,USA:KluwerAcademic Publishers.1992.1f2):275.288. ?5314?