Real-Time Symbolic Model Checking for Discrete Tim

Real-TimeSymbolicModelCheckingforDiscreteTimeModelsSergioV.CamposEdmundM.ClarkeMay2,1994CMU-CS-94-146SchoolofComputerScienceCarnegieMellonUniversityPittsburgh,PA15213ToappearinT.Rus,C.Rattray,editors,AMASTSeriesinComputing:TheoriesandExperiencesforReal-TimeSystemDevelopment.WorldScienticPublishingCompany.ThisresearchwassponsoredinpartbytheNationalScienceFoundationundergrantno.CCR-8722633,bytheSemiconductorResearchCorporationundercontract92-DJ-294,andbyTheDefenseAdvancedResearchProjectsAgency,InformationScienceandTechnologyOce,underthetitle\ResearchonParallelComputing,ARPAOrderNo.7330,issuedbyDARPA/CMOunderContractMDA972-90-C-0035.Theviewsandconclusionscontainedinthisdocumentarethoseoftheauthorandshouldnotbeinter-pretedasrepresentingtheocialpolicies,eitherexpressedorimplied,ofNSF,SRC,ortheU.S.government.Keywords:SymbolicModelChecking,Real-timeSystems,PriorityInversionAbstractThebdd-basedsymbolicmodelcheckingalgorithmgivenin[4,10]isextendedtohandlereal-timepropertiesusingtheboundeduntiloperator[9].Webelievethatthisalgorithm,whichisbasedondiscretetime,isabletohandlemanyreal-timepropertiesthatariseinpracticalproblems.Oneexampleofsuchapropertyispriorityinversion.Thisisaseriousproblemthatcanmakereal-timesystemsunpredictableinsubtleways.Ourworkdiscussesthisproblemandpresentsonepossiblesolution.Thesolutionisformalizedandveriedusingthemodiedalgorithm.Wealsoproposeanotherextensiontothemodelcheckingalgorithm.Timedtransitiongraphsaretransitiongraphsinwhicheventsmaytakenon-unittimetooccur.ThetimeittakesforatransitioninaTTGtohappenisdeterminedbyatimeinterval.Thisallowstheconstructionofsmallerandmorerealisticmodels.AsymbolicmodelcheckingalgorithmisgivenforformulasusingtheboundeduntiloperatorinTTGmodels.1IntroductionTemporallogicmodelcheckingisatechniquefordeterminingthecorrectnessofnite-statesystems.Alargenumberofproblemsincomputersciencecanbemodeledusingnite-staterepresentations.Real-timesystemscanoftenberepresentedinsuchaway.Becausetheyareusedinmanycriticalapplications,beingabletodependonthemisvital.Modelchecking[5,6]canassistindemonstratingthecorrectnessofsuchsystems.Theuseofthistechniquecanhelpincreasetheeciencyoftheirvalidationandhelpgeneratesystemswithhigherreliability.Thisworkexplainshowmodelcheckingcanbeappliedtothevericationofreal-timesystems.Inmodelchecking,specicationsareexpressedasformulasofapropositionaltemporallogic.Thesystemtobeveriedismodeledasastate-transitiongraph,andthegraphissearchedtodetermineifitsatisestheproperty.Asymbolicmodelcheckingalgorithmisoneinwhichthetransitionrelationisrepresentedimplicitlybybooleanformulas,andstatesarenotexplicitlyenumerated.TheSMVsymbolicmodelcheckingalgorithm[4,10]isthebasisofourapproach.Itisextendedtohandlereal-timeproperties.TheoriginalmodelcheckingalgorithmrepresentspropertiesasformulasinthetemporallogicCTL(ComputationTreeLogic).Thislogicallowsustostatepropertiessuchas\eventpwillhappensometimeinthefuture,butnot\eventpwillhappeninatmostxunitsoftime.Inreal-timesystemspropertiesofthelattertypeappearfrequently,becausewemustboundtheexecutiontimeinordertomakethesystempredictable.WeaugmentCTLsothatitispossibletoexpressreal-timepropertiesusingtheboundeduntiloperator[9],andshowhowtocheckformulasinvolvingoperatorsofthistypeusingbdd-basedsymbolicmodelcheckingtechniques.AnotherextensiontothealgorithmcomesfromthefactthatalltransitionsinaSMVmodeltakeexactlyonesteptooccur.However,inrealisticmodelsthisisnotalwaystrue.Varioustransitionsfrequentlyhavedierentlengthsinpractice.Itisalsopossiblethatonetransitioncantakedierentamountsoftimetooccurindierentexecutions.ModelingthisbehaviorinSMVcanbeachievedbyexpandinganon-unittransitionintoasequenceoftransitionsthroughseveralintermediatestates.Thestatesintroducedbythistechniquemaysignicantlyincreasethesizeofthemodel.WeproposeanextensioncalledTimedTransitionGraphs(TTG)tohandlethissituation.ATimedtransitiongraphisatransitiongraphthathastimeintervalsassociatedwithtransitions.Thetimeintervalsspecifyalowerandanupperboundonthetimeittakesforatransitiontooccur.Atransitioncantakeanondeterministicnumberofstepstooccur,withintheboundsspeciedbytheTTG.Longertransitionsthatarealsonon-deterministic(withinspeciedbounds)allowthemodelingofrealisticsystemswithouttheburdenofaddingextrastatestothemodel.AsymbolicmodelcheckingalgorithmispresentedforboundedCTLformulasusingTTGsasmodels.Asanexampleofhowthesetechniquescanbeused,wemodelthepriorityinversion[8,11]problemusingtheextendedverier.Mostreal-timesystemsrelyonprioritiestomaintainpredictability.Thefactthathigherprioritytasksmustbeexecutedbeforelowerprioritytasksisessentialforthecorrectnessofsuchsystems.However,lowpriorityprocessescanblockhighpriorityprocessesindenitely,becauseofindirectpriorityconstraints.Thissituationiscalledpriorityinversion.Thisbehaviormakesthesystemunpredictable.Itisdescribedinthispaper.Severalsolutionsexisttothisproblem,andoneofthose,priorityinheritance,is1presentedandformallyveried.Temporallogicmodelcheckingisdescribedinsection2.Section3discussesbinarydecisiondiagrams,whic