搜索
3)(No.60573085)973(No.2002CB312001),;,,;,,;,,2007Vol134113)(,210093),x-y()n,,,,,,,,,,AnAlgorithmtoDynamicallyReducetheStateSpaceofTimedAutomataduringtheReachabilityAnalysisCHENMing2SongZHAOJian2HuaLIXuan2DongZHENGGuo2Liang(NationalLaboratoryofNovelSoftwareTechnology,DepartmentofComputerScienceandTechnology,NanjingUniversity,Nanjing210093)AbstractThereachabilityanalysisalgorithmexploresthestatespaceofatimedautomatonbyenumerationofsymbolicstates.Eachsymbolicstateconsistsofalocationandatimezonewhichareconjunctionsofautomaticformulaeintheformx-y()n.Sometimestheamountofgeneratedsymbolicstatesisverylarge,thememoryrequiredtostorethegeneratedsymbolicstatesisnotfeasible.Inthispaper,wepresentanapproachtoreducethememoryrequirementofthereachabilityanalysisalgorithm.Byanalyzingthedependencerelationbetweensymbolicstates,wecanexpandsomeofthesymbolicstatesbyremovingspecifickindsofatomicformulaewithoutchangingthereachabilityanalysisre2sult.Theexpandedstatescancontainmoresymbolicstates.Removingthesecontainedstatescanreducethememoryrequirementofreachabilityanalysis.Thecasestudiespresentedinthispapershowthatouralgorithmcansavememoryinthepracticalapplicationefficiently.KeywordsTimedautomata,Modelchecking,Symbolicstate,Timezone1(modelchecking)[1],(timedau2tomaton)[2],,,,,(concretestate),R+,::,,,,,[3];[4]x0(),x0-y()n(y-x0()n)[5]312,,,,2,,34,52,2.1G(C)Cxn(xC,nN,{,,,})(N,l0,C,E,I):(1)N;(2)l0N,C;(3)EANG(C)2CN;(4)INlI(l),I(l)G(C),x()n,n(l1,g,r,l2),l1,g,,l2,r0,(l,v),l,vCR+xC,v(x)R+(l,v)x,(,),()1:(1):dR+,v+dl,(l,v)d(l,v+d),v+dxC,(v+d)(x)=v(x)+d;(2):e=(l1,g,r,l2),vg,(l1,v)e(l2,v),v:c,cr,v(c)=0,v(c)=v(c)2.2,,,C,B(C)C(timezone),x-yn(x,yC{0},{,},nZ)xn(nN)x-0()n,0-x()-n,C,G(C)AB(C)D1D2D2]D1,D1D2,D2AD1D2AD1D1AD2,D1D2d1(x-y1c1)d2(y-z2c2),x-z3c1+c2d1d2,,12,3,3,d1d2,d1d2(l,D),l,D,DB(C)(l,D){(l,v)|vD}SP(e,(l,D)){(l,v)|ve,d,(l,v)vD(l,v)e(l,v)d(l,v)}e=(l,g,r,l),SP(e,(l,D))(l,(r(Dg))I(l)),I(l)l,r(D)cr,r(D)Dc,Dcup,D[6],r(x),:(1)r(D)dD,x0({=,})(2)DdD(3)D1D2D1,D2(4)D,DD,DD,D2.3,,SP:(1);(2)PASSED={};WAITING={(l0,D0)};412repeatWAITING(l,D),S,WAITING=WAITING-{S};le,beginifSP(e,S),then;S=SP(e,S),S=(l,D);ifll1,then;ifS=(l,D)WAITINGPASSEDDAD,thenSS;elseWAITING=WAITING{S},SS;endSPASSED;untilWAITING={}11,[79](l0,D0),l1,WATINGPASSEDWATING;PASSED,PASSEDWAITING,,,,1SSee(SeSe),S=(l,D),Se=(l,D),SP(e,(l,D))ASeSeSe,SSee2.4,WAITING,,(l,D)eSP(e,(l,D))=(l,D)(r(Dg))I(l)),SP(e,(l,D))D,g,{x0|xr,{=,}}23,:(1)(l,D)eSP(e,(l,D))(l,D),DdDdddD,g{x0|xr,{,}}(2)SSe,SSeeSex-yc(x,y0,{,})SdSP(e,(l,D))x-yccc,x-ycd(3)SS,SdSdSe1S1e2S2Sn(=S),i(1in-1),Sidi,ddn-1,didi-1(2in-1)d1d31,PASSED,WAITING,[4],,,,1,PASSED(l,D),(l,D)PASSED,,,,PASSEDPASSED1WAITING,PASSEDPASSED(l,D)(l,D),DAD,,DDDDAD,DAD,D¾D;,PASSED(l,D)(l,D);,WAITING(l,D)(l,D)PASSED,(l,D)(l,D),(l,D)1FALSE,3SSe1,e2,e3,,en-1,enSe1S1e2S2enSn=S(n1),SSP=e1,e2,e3,,en-1,en(n1),SP,SP(P,(l,D))=SP(en,,SP(e2,SP(e1,(l,D)))),,,(l,D)PASSED,DD,DAD1,(l,D)(l,D)lp,SP(p,(l,D)),SP(p,(l,D))1,(l,D)(l,D),(l,512D)(l,D),(l,D)1,(l,D),(l,D)(l,D),1[4]1(l,D)e=(l,g,r,l),DAAgADSP(e,(l,D)),1,d,d,d1,,,,,1,,,,,,,,,:4,:(relevant),(irrelevant),(unknown)(1)(relevant):a)(l,D)e,A,Ab)(l,D)A,(l,D),Ac)(2)(unknown):a)(l,D),e1,e2,,enl,Db)(l,D)A,(l,D),A,(3)(irrelevant):,,,2TagDepAF(atomicF,type)atomicFatomicFtypeTagUnknown2AF(WATING)WATINGUNKNOWNTagReleventAF(af)afRELEVENT,TagReleven2tAF(af)=TagDepAF(af,RELEVENT)RemoveIrrelev2entAF(),:RELEVENTUNKNOWN(NULL);;NULLTagDepAF(atomicF,type)BeginatomicFtype;foratomicFPreSTbeginifPreSTPreAFatomicFthenTagDepAF(PreAF,type);elsereturn;endendTagUnknownAF(WATING)beginforWATINGSbeginforSafbeginTagDepAF(af,UNKNOWN);endendend244.13,,:initState(NULL),curState,curState,,PASSED4WAITING,WAITING,PASSEDWAITING,WAITINGPASSED,,,PASSED,,,4.236123,:e1=(l,x1,ª,l1),e2=(l,x1,{z},l2),,PASSEDS1=(l,x2y1z3)S2=(l,x2y1z2),S3=(l2,x2y1)WAIT2INGS1e1S2e1ª,S1e2S2e2S3WAIT2ING3,S1S2x2,;y1,S1z3S2z2S1S2,,,,,PASSED,,CPU,4.3,,,,,PASSED,,4,,PASSED={};WAITING={(l0,D0)},D0;repeatWAITING(l,D),S,WAITING=WAITING-{S};forle,beginifWAITINGPASSEDthenbeginTagUnknownAF(WAITING);RemoveIrreleventAF();if,then;endifSP(e,S),SkafthenTagReleventAF(kaf),;S=SP(e,S)=(l,D);ifll1,then;ifS=(l,D)WAITINGPASSEDDADthenSS;elseWAITING=WAITING{S}SS;endSPASSED;untilWAITING={}45C++4,50000,,,PASSED,,,,3.62GProLiant,Fischer(Fis2chersmutualexclusionprotocol),Bang&Olufsion(theBang&Olufsionaudioprotocol)[10]CSMA/CD(CarrierSenseMultipleAccesswithCollisionDetectionpro2tocol)Fischer,,Bang&Olufsion/Bang&Olufsion,1125698136111,39s;10000,4,60446590,378s;,80718822,268s[35]1CSMA/CDprotocolOptimizationMethods(nodes/runtime)BasicStaticIAFRDynamicIAFRStatic+DynamicIAFRCSMA53580/2664/1550/1550/1CSMA625905/792057/11800/41800/1CSMA7N/A6026/25000/245000/1CSMA8N/A16907/513000/16413000/12CSMA9N/A45836/2133000/127033000/84CSMA10N/A120845/9690000/2332890000/105CSMA11N/A311310/325N/A250000/303CSMA12N/A786447/1267N/A600000/1251CSMA/CD1:1BASICStaticIAFR(StaticIrreleventFormulaeRe2moval)[4]4DynamicIAFR(Dynam2icIrreleventFormulaeRemoval)Static+DynamicIAFR,,,,N/712A1,[4],,,,,,,,,,,,,1ClarkeEMJr,GrumbergO,PeledDA.