Model-checking for real-time systems

Model{CheckingforReal{TimeSystems?KimG.Larsen1PaulPettersson2WangYi21BRICS???,AalborgUniversity,DENMARK2UppsalaUniversity,SWEDENAbstract.Ecientautomaticmodel{checkingalgorithmsforreal-timesystemshavebeenobtainedinrecentyearsbasedonthestate{regiongraphtechniqueofAlur,CourcoubetisandDill.However,thesealgo-rithmsarefacedwithtwopotentialtypesofexplosionarisingfrompar-allelcomposition:explosioninthespaceofcontrolnodes,andexplosionintheregionspaceoverclock-variables.Thispaperreportsonworkattackingtheseexplosionproblemsbydevel-opingandcombiningcompositionalandsymbolicmodel{checkingtech-niques.Thepresentedtechniquesprovidethefoundationforanewauto-maticvericationtoolUppaal.ExperimentalresultsshowthatUppaalisnotonlysubstantiallyfasterthanotherreal-timevericationtoolsbutalsoabletohandlemuchlargersystems.1IntroductionWithinthelastdecademodel{checkinghasturnedouttobeausefultech-niqueforverifyingtemporalpropertiesofnite{statesystems.Ecientmodel{checkingalgorithmsfornite{statesystemshavebeenobtainedwithrespecttoanumberoflogics.However,themajorprobleminapplyingmodel{checkingeventomoderate{sizesystemsisthepotentialcombinatorialexplosionofthestatespacearisingfromparallelcomposition.Inordertoavoidthisproblem,algo-rithmshavebeensoughtthatavoidexhaustivestatespaceexploration,eitherbysymbolicrepresentationofthestatesspaceusingBinaryDecisionDiagrams[5],byapplicationofpartialordermethods[11,21]whichsuppressesunnecessaryinterleavingsoftransitions,orbyapplicationofabstractionsandsymmetries[7,8,10].Inthelastfewyears,model{checkinghasbeenextendedtoreal{timesystems,withtimeconsideredtobeadenselinearorder.Atimedextensionofniteautomatathroughadditionofanitesetofreal{valuedclock{variableshasbeenputforward[3](socalledtimedautomata),andthecorrespondingmodel{checkingproblemhasbeenprovendecidableforanumberoftimedlogicsincludingtimedextensionsofCTL(TCTL)[2]andtimed{calculus(T)[14].?ThisworkhasbeensupportedbytheEuropeanCommunietiesunderCONCUR2,BRA7166,NUTEK(SwedishBoardforTechnicalDevelopment)andTFR(SwedishTechnicalResearchCouncil)???BasicResearchinComputerScience,CentreoftheDanishNationalResearchFoundation.Astateofatimedautomatonisoftheform(l;u),wherelisacontrol{nodeanduisaclock{assignmentholdingthecurrentvaluesoftheclock{variables.ThecrucialobservationmadebyAlur,CourcoubetisandDillandthefoundationfordecidabilityofmodel{checkingisthatthe(innite)setofclock{assignmentsmayeectivelybepartitionedintonitelymanyregionsinsuchawaythatclock{assignmentswithinthesameregioninducestatessatisfyingthesamelogicalproperties.Model{checkingofreal{timesystemsbasedontheregiontechniquesuerstwopotentialtypesofexplosionarisingfromparallelcomposition:Explosionintheregionspace,andExplosioninthespaceofcontrol{nodes.Wereportonat-tacksontheseproblemsbydevelopmentandcombinationoftwonewvericationtechniques:1.Asymbolictechniquereducingthevericationproblemtothatofsolvingsimpleconstraintsystems(onclock{variables),and2.Acompositionalquotientconstruction,whichallowscomponentsofareal{timesystemtobegraduallymovedfromthesystemintothespecication.Theintermediatespecicationsarekeptsmallusingminimizationheuristics.Theproperty-independentnatureofregionsleadstoanextremelyne(andlarge)partitioningofthesetofclock{assignments.Oursymbolictechniqueallowsthepartitioningtotakeaccountoftheparticularpropertytobeveriedandwillthusinpracticebeconsiderablycoarser(andsmaller).Fortheexplosiononcontrol{nodes,recentworkbyAndersen[4]on(un-timed)nite{statesystemsgivesexperimentalevidencethatthequotienttech-niqueimprovesresultsobtainedusingBinaryDecisionDiagrams[5].Theaimoftheworkreportedistomakethisnewsuccessfulcompositionalmodel{checkingtechniqueapplicabletoreal{timesystems.Forexample,considerthefollowingtypicalmodel{checkingproblemA1j:::jAnj=’wheretheAi’saretimedautomata.Wewanttoverifythattheparallelcompo-sitionofthesesatisestheformula’withouthavingtoconstructthecompletecontrol{nodespaceof(A1j:::jAn).WewillavoidthiscompleteconstructionbyremovingthecomponentsAionebyonewhilesimultaneouslytransformingtheformulaaccordingly.Thus,whenremovingthecomponentAnwewilltransformtheformula’intothequotientformula’=AnsuchthatA1j:::jAnj=’ifandonlyifA1j:::jAn1j=’=An(1)Nowclearly,ifthequotientisnotmuchlargerthantheoriginalformulawehavesucceededinsimplifyingtheproblem.RepeatedapplicationofquotientingyieldsA1j:::jAnj=’ifandonlyif1j=’=An=An1=:::=A1(2)where1istheunitwithrespecttoparallelcomposition.However,theseideasaloneareclearlynotenoughastheexplosionmaynowoccurinthesizeofthenalformulainstead.Thecrucialandexperimentally\veriedobservationbyAndersenwasthateachquotientingshouldbefollowedbyaminimizationoftheformulabasedonasmallcollectionofecientlyimplementablestrategies.Inoursetting,Andersen’scollectionisextendedtoincludestrategiesforpropagatingandsimplifyingtimingconstraints.Wereportonanewsymbolicandcompositionalvericationtechniquedevelopedforthereal{timelogicsL[17]andafragmentLsdesignedspeci-callyforexpressingsafetyandboundedlivenessproperties.ComparativelylessexpressivethanTCTLandT,thefrag