ofComponent-BasedSoftwareSystems
JeffreyJ.P.TsaiandEricY.T.Juan
DepartmentofElectricalEngineeringandComputerScience
UniversityofIllinois,Chicago851S.MorganSt.,Chicago,IL60607
Email:tsai@eecs.uic.edu
Abstract
Withtherapidgrowthofnetworkingandhigh-computingpower,thedemandoflargerandmorecomplexsoftwaresystemshasincreaseddramatically.Todealwiththecomplexityinde-signinglarge-scalecomplexsoftwaresystems,theconceptofcomponent-basedsoftwaredesignhasgainedpopularityrecently.However,inpursuingacomponent-basedapproachthereareob-staclestobeovercome.Oneofthemisthestate-explosionproblemintheformalverificationoflarge-scalecomponent-basedsystems.Inthispaper,weintroduceamodelingtechniqueandtwocondensationtheoriestomodelandverifycomponent-basedsoftwaresystems.Ourconden-sationtheoriesaremuchweakerthancurrenttheoriesusefulforthecompositionalverification.Moresignificantly,ournewcondensationtheoriescaneliminatetheinterleavedbehaviorscausedbyasynchronouslysendingactions.Therefore,ourtechniqueprovidesamuchmorepowerfulmeansforthecompositionalverificationofasynchronousprocesses.Ourtechniquecaneffi-cientlyanalyzeseveralstate-basedproperties:deadlockstateandreachablestate.Theexperi-mentalresultsshowasignificantimprovementintheanalysisoflarge-scalecomponent-basedsystems.
1INTRODUCTION
Withtherapidgrowthofnetworkingandhigh-computingpower,thedemandoflargerandmorecomplexsoftwaresystemshasincreaseddramatically.Examplesincludeweb-basedsys-tems,multimediasystems,telecommunicationsystems,intelligentagentssystems,flightcontrolsystems,patiencemonitoringsystems,robotics,virtualrealitysystems,andsoon.However,thedevelopmentoflarge-scaleandcomplexsoftwaresystemsismuchmoredifficultanderrorprone.Thisisduetothefactthattechniquesandtoolsforassuringthecorrectnessandreliabilityofsoft-waresystemslagfarbehindtheincreasinggrowthofsizeandcomplexityofsoftwaresystems.Theresultsareunreliableandpoorlyperformingapplications,delayedprojects,andconsider-ablecostoverruns.Inordertoimprovetheusabilityandreliabilityoflarge-scalesystems,thesupportingtechniquesanddevelopmenttoolsneedtobegreatlyenhanced.
Formalverificationisrapidlybecomingacceptedasapromisingandautomatedmethodtoverifythecorrectnessofsoftwaresystems.Despitemanyworksintheareaofformalverification,oneofmainbottleneckssofaristhestateexplosionproblem.Whenthesizeofasoftware
systemincreaseslinearly,theanalysiscomplexityofthesystemcouldgrowexponentially.Thecapabilityandperformanceofcurrenttechniquesstillcannotefficientlyverifytypicallarge-scalesoftwaresystemsinpractice.
Atechnique“compositionalverification”,whichisconsideredmoresuitableforanalyzingwell-definedsubsystems,suchascomponent-basedsystems,hasbeenproposedbyresearcherstodealwiththestate-explosionproblemoflarge-scalesystems.However,currentcompositionalverificationtechniquesareefficientonlyforverifyingevent-basedpropertiesofsynchronouspro-cesses.Inthispaper,weintroduceamodelingtechniqueandtwocondensationtheoriestomodelandverifycomponent-basedsoftwaresystems.Ourcondensationtheoriesaremuchweakerthancurrenttheoriesusefulforthecompositionalverification.Moresignificantly,ournewcondensa-tiontheoriescaneliminatetheinterleavedbehaviorscausedbyasynchronouslysendingactions.Therefore,ourtechniqueprovidesamuchmorepowerfulmeansforthecompositionalveri-ficationofasynchronousprocesses.Ourtechniquecanefficientlyanalyzeseveralstate-basedproperties:deadlockstateandreachablestate.Theexperimentalresultsshowasignificantim-provementintheanalysisoflarge-scalecomponent-basedsystems.
2THEMODEL
Thissectionintroducesamodel,namelymultisetlabeledtransitionsystems(MLTSsinthesequel).MLTSsarecloselyrelatedtolabeledtransitionsystems(LTSsforshort)whichareintensivelyusedasastate-spacemodelinthefamilyofprocessalgebras.Therearethreedis-tinguishingfeaturesbetweenMLTSsandtraditionalLTSs.First,thelabelofatransitionisamultisetofactionsinMLTSsinsteadofoneactioninLTSs.Second,wemakeacleardistinc-tionbetweensynchronouslycommunicatingactionsandasynchronouslycommunicatingactions.Third,thecompositionoftraditionalLTSsisforsynchronousprocessesonly,whilethecomposi-tionofbothsynchronousandasynchronousprocessescanbeachievedinMLTSs.ThesefeaturesofMLTSspromisethedevelopmentofanewmechanismforcompositionalverification.Withtheuseofthenewmechanism,thehighanalysiscomplexityoflarge-scalesystemscansignificantlybereduced.
SERVERReadyReceive-ReqSend-dataRetrieve-data
Figure1:MLTSspecificationofaserver.
ThebehaviorofaprocesscanbemodeledbyanMLTS.AnMLTSconsistsofstates,transi-tions,actions,andoneinitialstate.IngraphicalrepresentationofMLTSs,astateisdenotedbyashadedcircle,andatransitionbyasolidarrowlabeledwithactions.Theinitialstateispointedoutbyadottedarrow.
AstateinMLTSscouldbeinterpretedasacondition.ThestatesofanMLTSdescribethepossibleconditionsofaprocess.Forinstance,Figure1givesanMLTSwhichspecifiesaserver.TheconditionofSERVERiseitherreadytoacceptarequest(stateReady)orbusyinretrievingdata(stateRetrieve-data).ThestateofanMLTSischangedbytheexecutionofactions.OnceSERVERperformstheactionofreceivingrequest(Receive-Req),theconditionofSERVERis
changedfromstateReadytostateRetrieve-data.TheconditionofSERVERreturnstostateReadyafterSERVERsendsoutdata(actionSend-data).Aninitialstateistheconditionatthebeginning.TheinitialstateofSERVERisReady.
Therelationshipofstatesandactionsisrepresentedbytransitions.Atransitioncontainsastartingstate,oneormoreactions,andanendingstate.Forexample,transition(Ready,Receive-Req,Retrieve-data)indicatesthatstateRetrieve-dataisreachablefromstateReadybytheexe-cutionofactionReceive-Req.Inthefollowing,wefirstgivetheformaldefinitionofMLTSs.Definition2.1MultisetLabeledTransitionSystems(MLTSs)Amulti-setMSconsistsofasetDandamappingMS:DN,whereN=1,2,3,...isthesetofpositiveintegers.MSissaidtobeamulti-setofasetSiff(ifandonlyif)DS.AMLTSisaquadruple(S,,T,s),where1)Sisasetofstates;sistheinitialstate;
,whichisasetofactions(transitionlabels),comprisesinvisible(orinternal)action()2)
andcommunicatingactions,whereconsistsof(synchronouslycommunicatingac-(asynchronouslysendingactions),and(asynchronouslyreceivingactions);tions),and
3)TSMSisasetoftransitionssuchthat(s,m,s’)T:misanon-emptymultisetof.
InMLTSs,atransitionislabeledwithamultisetofactions.Amultisetconsistsofcount-ableobjects.Thismeansthatanactioncanhavemultipleinstancesinatransitionlabel.Weusesynchronouscommunicationand/orasynchronouscommunicationastheprimitivemeansof
)inMLTSsarecommunicationbetweenprocesses.Synchronouslycommunicatingactions(
usedtospecifyunbufferedmodeofsynchronouscommunicationwhichisusuallyreferredtoashandshakingorrendezvouscommunication.Synchronouscommunicationbetweenprocessesisperformedthroughasimultaneousexecutionofactionswhichreadfromorwritetoasharedchannel.Inotherwords,actionswhichreadfromorwritetoasharedchannel,havetotakeplaceatthesametime.
ThesemanticsofasynchronousinteractionofMLTSsisessentiallythesameasasynchronousmessagepassingusedinNIL[5]andPLITS[2].Inasynchronouscommunication,asendingprocessisnotblockedtowaitforitscommunicatingpartners.Onceamessageisready,theprocessisfreetoperformitsasynchronouslysendingaction.Messageswhichhavenotbeenreceivedbyreceiversarestoredinthebuffersofchannels.InMLTSs,thechannelbuffersofasynchronouscommunicationhaveunboundedcapability.Anasynchronouslyreceivingprocess,asinthecaseofsynchronouscommunication,maybeblockedinordertowaitformessages.Notethatchannelsforsynchronouscommunicationhavenobufferforthestorageofmessages,sincesynchronouscommunicationbetweenprocesseshastotakeplaceatthesametime.
3DEADLOCKSTATEANDREACHABLESTATE
Inthissection,wefocusonthepropertiesofdeadlockstatesandreachablestates.AstateissaidtobereachableinanMLTSifthestatecanbereachedfromtheinitialstateviadirectededges.RecallthatastateinMLTSscouldbeinterpretedasacondition.Thus,areachablestatecanbeconsideredasapossibleconditionthataprocessorsystemcanreach.
Asystemissaidtobedeadlockingifthesystemhasreachedacondition(state)suchthatthesystemcannotdoanything.Inpractice,adeadlockstatereflectsafailureorsuccessfulterminationofasystem.Inordertodistinguishfailurefromsuccessfultermination,wepreservetheconditionsofdeadlockingsystems,i.e.,deadlockstates.Fromtheinspectionofdeadlockstates,wecaneasilydeterminewhetheradeadlockingsystemfailsorsuccessfullyterminates.Inaddition,adeadlockstate,whichprovidesdetailedconditionsofthewholesystem,isusefulfordebuggingandmodifyinganimpropersystemdesign.ThefollowingdefinesreachablestatesanddeadlockstatesinMLTSs.
Definition3.1(ReachableStates)
,T,s)beanMLTS.Astatesisreachablein(S,,T,s)iffLet(S,
1)s=sor2)(s,m,s)(s,m,s)suchthati),ii)s=s,iii)s=s,andiv)1jn:(s,m,s)T.
Definition3.2(DeadlockStates)Let(S,,T,s)beanMLTS.Astatesisadeadlockstateof(S,,T,s)iff1)sisreachablein(S,,T,s)and2)(s,m,s’)T(shasnooutgoingtransition).
4CONDENSATIONTHEORIESFORMLTSs
Thissectionpresentsournewlyderivedcongruencetheoriesforthecompositionalverificationofdeadlockstatesandreachablestates.WecallourcongruencetheoriesIOT-failureequivalenceandIOT-stateequivalence.IOT-failureequivalencepreservesthepropertyofdeadlockstateswhileIOT-stateequivalencepreservesthepropertyofreachablestates.Wewillexplainthesetwocongruencetheoriesusingsimpleexamples.
4.1PathsandInput/Output-Traces(IO-Traces)
ThecomputationofanMLTScanbedescribedintermsofpaths.ApathisanalternatingsequenceofstatesandtransitionsinMLTSs.Forexample,MLTSPinFigure2hasapath
=s,(s,Ch,s),s,(s,Ch!,s),s,(s,Ch!,s),s,(s,Ch,s),s.
Forsimplicity,wealsowritepathas
s,Ch,s,Ch!,s,Ch!,s,Ch,s.
Similarly,MLTSPinFigure2hasapath
=s,(Ch,Ch!,Ch!),s,Ch,s.
PathmeansthatifthelocalconditionofMLTSPisstates,thenPisreadytosequen-tiallyexecuteactionsCh,Ch!,Ch!,Chandtosequentiallyreachstatess,s,s,s.However,theexecutionalongpathmayfailduetosomeconditionoutsideMLTSP,i.e.,theenvironmentconditionofP.Inotherwords,fortheoccurrenceofapathtobesuccessful,weneedtoconsidertheglobalconditionwhichconsistsofalocalconditionandanenvironmentcondition.
WeuseIO-tracesinordertodeduceandcomparetheglobalconditionsrequiredfortheoc-currencesofpaths(actions).IO-tracesarederivedfrompathsbyremovingsomedetailswhichareirrelevanttothesuccessofpaths’occurrences.BasedonIO-traces,wehavedevelopedIOT-failureequivalenceandIOT-stateequivalenceaspresentedinthefollowingsections.
P70P80Ch1 Ch2 !Ch3 !321τ12Ch4Ch5 ?5Ch44
P7-C0P8-CCh1, Ch2!, Ch3! Ch5 ?3Ch454
Ch1 Ch1 02Ch433Ch2in=0, Ch3in=0, Ch5in=1
Figure2:ExampleofpathsandIO-traces.
AnIO-traceconsistsofi)astartingstate,ii)anendingstate,andiii)asequenceofmultisetsofactions.Informallyspeaking,anIO-traceisderivedfromapathby1)removingintermediatestates,
2)replacingatransitionwithtwoorderedelements(multisets),i.e.,i)itsenvironmentpre-conditionandthenii)itsenvironmentpost-condition,3)removingemptymultisetsofactions,and
4)summingupadjacentmultisetsofenvironmentpost-conditions.
Theenvironmentpre-conditionofatransitionconsistsofsynchronouslycommunicatingac-tionsandasynchronouslyreceivingactionswhicharelabeledonthetransition.Theenvironmentpost-conditionofatransitionisrepresentedbyasynchronouslysendingactionslabeledonthetransition.Theexecutionofinvisibleactionsdoesnotinteractwiththeenvironment.Therefore,invisibleactionsarenotincludedinIO-traces.LetusconsiderMLTSsinFigure2asanexam-ple.AssumethatChandCharesynchronouscommunicationchannelsbetweenprocessesPandP.Itisclearthattheenvironmentpre-conditionoftransition(s,Ch,s)isCh;theenvironmentpost-conditionoftransition(s,Ch,s)isnull.NowletusderivetheIO-traceforthepath=s,Ch,s,Ch!,s,Ch!,s,Ch,sinMLTSPabove.After1)removingintermediatestatess,sands,and2)replacingatransitionwithitsenvironmentpre-conditionandthenitsenvironmentpost-condition,weget
s,Ch,,,Ch!,,Ch!,Ch,,s.
Afterthat,weremoveemptymultisetsofactionsandsumupadjacentmultisetsofenvironment
ispost-conditions(orasynchronouslysendingactions).Asaresult,theIO-traceofpath
IOT=s,Ch,Ch!,Ch!,Ch,s.
Similarly,wecanderivetheIO-traceofpath=s,(Ch,Ch!,Ch!),s,Ch,sinMLTSPaboveas
IOT=s,Ch,Ch!,Ch!,Ch,s.
Frompathsand,wecanseethattwodifferentpathsmighthaveanidenticalIO-trace.IO-tracesareusefulforpredictingthesuccessfuloccurrencesofpaths(oractions).BasedonIO-traces,IOT-failureequivalenceandIOT-stateequivalencewillbepresentedinthefollowingsections.
4.2IO-TraceFailures(IOT-Failures)
Inordertoefficientlyanalyzealarge-scalesystem,itisdesirabletoeliminatedatawhichareir-relevanttotheverificationofinterestingproperties.OurIOT-failureequivalenceisdevelopedforthecompositionalverificationofdeadlockstates.ThismeansthatIOT-failureequivalentMLTSsareinterchangeableinthecompositionalverificationofMLTSswithoutlossofanydeadlockstate.IOT-failureequivalenceisveryusefulforreducingthesize(complexity)ofMLTSswhenwefocusonthepropertyofdeadlockstates.
Informallyspeaking,anIOT-failureforanMLTSisapairconsistingofi)anIO-tracetstartingfromtheinitialstateandii)thesetofenvironmentpre-conditionsfortheoutgoingtransitionsoftheendingstateoft.Inaddition,theendingstateoftheIO-tracetaboveshouldbestable.
Astatesissaidtobestableiffsdoesnothaveanyout-transitionwhoseenvironmentpre-conditionisempty;otherwisesisnon-stable.Inotherwords,onlystablestatesarecandidatesfortheconstructionofdeadlockstates,becauseanon-stablestatehasatleastoneout-transitionwhichisguaranteedtobeexecutableinanyconditionoftheenvironment.
LetusconsiderMLTSPinFigure2asanexample.InMLTSP,bothtransitions(s,Ch!,s)and(s,Ch!,s)haveanemptyenvironmentpre-conditionbecausetheyexecuteneithersynchronouslycommunicatingactionnorasynchronouslyreceivingaction.Therefore,statessandsarenon-stable.Incontrast,statess,s,s,andsarestable.ThesestablestatesarereachedfromtheinitialstatesviathefollowingIO-tracesrespectively:
IOT=s,,s,
IOT=s,Ch,Ch!,Ch!,s,
IOT=s,Ch,Ch!,Ch!,Ch,s,andIOT=s,Ch,Ch!,Ch!,Ch?,s.
FromthesestablestatesandIO-traces,wegetfourIOT-failuresinMLTSP:
IOTF=(IOT,Ch),
IOTF=(IOT,Ch,Ch?),IOTF=(IOT,),andIOTF=(IOT,).
IOT-failuresIOTFandIOTFhaveanemptysetofenvironmentpre-conditionssincestatessandshavenoout-transition.Stateshastwoout-transitions(s,Ch,s)and(s,Ch,s).Transition(s,Ch,s)hasanenvironmentpre-conditionCh,andtransition(s,Ch,s)hasanenvironmentpre-conditionCh?.Therefore,thesetofenvironmentpre-conditionsofIOT-failureIOTFisCh,Ch?.
andaresaidtobeIOT-failureequivalentiffandhavethesamesetTwoMLTSs
ofIOT-failures.Forinstance,PinFigure2alsohasfourIOT-failuresIOTF,IOTF,IOTF,andIOTF.Thus,MLTSsPandPinFigure2areIOT-failureequivalent.Similarly,MLTSsPandPinFigure2areIOT-failureequivalentaswell.
IOT-failureequivalenceisacongruenceintermsofdeadlockstates.Therefore,IOT-failureequivalentMLTSsareinterchangeableinthecompositionalverificationofMLTSswithoutlossofanydeadlockstate.Forexample,fromtheMLTSsinFigure2,wecancomposetwoMLTSsasshowninFigure3.WithoutverifyingthesetwoMLTSsinFigure3,wecanguaranteethattheyhavethesamesetofdeadlockstates,i.e.,sands.
P7 || P8 (Ch2in=0, Ch3in=0, Ch5in=1)
(1,1,0,0,1)(2,1,1,0,1)(3,1,1,1,1)(0,0,0,0,1)Ch1 τCh2 !Ch2 !τCh3 !Ch3 !τCh4(5,2,1,1,0)Ch5 ?(4,3,1,1,1)
(1,2,0,0,1)(2,2,1,0,1)(3,2,1,1,1)P7-C || P8-C (Ch2in=0, Ch3in=0, Ch5in=1)
(0,0,0,0,1)Ch1, Ch2 !, Ch3 ! (5,2,1,1,0)Ch5 ?Ch4(4,3,1,1,1)
(3,2,1,1,1)Figure3:Deadlock-stateequivalentMLTSs.
4.3IO-TraceStates(IOT-States)
IOT-stateequivalenceisdevelopedforthecompositionalverificationofreachablestates.AnIO-tracestate(IOT-state)isanIO-tracestartingfromtheinitialstate.TwoMLTSsaresaidtobeIOT-stateequivalentiftheyhavethesamesetofIOT-states.IOT-stateequivalenceisacongruenceintermsofreachablestates.ThismeansthatIOT-stateequivalentMLTSsareinterchangeableinthecompositionalverificationofMLTSswithoutlossofanyreachablestate.
P9Ch1 Ch1 τ012Ch2 34P9-C
Ch1 0123
Ch2 4Figure4:ExampleofIOT-statesandIOT-stateequivalentMLTSs.
Asasimpleexample,letusconsiderMLTSsPandPinFigure4.AssumethatChandCharesynchronouscommunicationchannels.Statess,s,andsinMLTSPareconciselyrepresentedbyamacrostateinMLTSP.WecanseethatMLTSsPandPareIOT-stateequivalentbecausetheyhavethesamesetofIOT-states:
IOTS=s,,s,IOTS=s,Ch,s,IOTS=s,Ch,s,IOTS=s,Ch,s,andIOTS=s,Ch,Ch,s.
5CONCLUSION
Thispaperpresentsanewmodelingtechniqueandtwonewcondensationtheoriestore-ducethestateexplosionproblemofasynchronousprocessesaswellassynchronousprocessesincomponent-basedsoftwaresystems.Ourcondensationtechniquehasreasonablecomplex-ity(polynomialinthenumbersofstatesandtransitions).Fromtheexperimentalresults,ourtechniquepromisesamuchmoreefficientanalysis,especiallyforasynchronousprocessesindistributedsystems.ThecondensationtheoriescanbeappliedtoPetrinetsmodeltoo[6].Thecurrentversionofourtechniquefocusesontheanalysisofdeadlockstatesandreachablestates.Nevertheless,webelievethatamoreelaboratedextensioncanbeusedtoverifymanyotherimportantsafetyandlivenesspropertiesofdistributedsystems,suchasaccessibilityandeventsequences.Anextensionofourworkiscurrentlyunderstudy.
6ACKNOWLEDGMENTS
ThisresearchwassupportedinpartbyNSFandDARPAunderGrantCCR-9633536.
References
[1]S.Brookes,C.Hoare,andA.Roscode,“Atheoryofcommunicatingsequentialprocesses,”ACM
31,3,pp.560-599,1984.[2]J.A.Feldman,“Aprogrammingmethodologyfordistributedcomputing(amongotherthings),”
CommunicationACM22,pp353-368,1979.[3]C.A.R.Hoare,CommunicatingSequentialProcesses,Prentice-Hall,EnglewoodCliffs,N.J.,1985.[4]R.Milner,“Operationalandalgebraicsemanticsofconcurrentprocesses,”Handbookoftheoretical
computerscience,ed.J.vanLeeuwen,ElsevierSciencePublisherB.B.,1990.[5]R.E.StromandN.Halim,“Anewprogrammingmethodologyforlong-livedsoftwaresystems,”
IBMJ.Res.Devel.28,pp.52-59,1984.[6]Y.T.Juan,J.J.P.Tsai,andT.Murata,”CompositionalVerificationofConcurrentSystemsUsing
Petri-Nets-BasedCondensationRules,”ACMTransactionsonProgrammingLanguagesandSys-tems,Vol.20,No.5,pp.917-979,Sept.1998.
因篇幅问题不能全部显示，请点此查看更多更全内容