Model Checking the Branching Time Temporal Logic C

fenggang2005316
2 ℃
2020-05-13

整理文档很辛苦，赏杯茶钱您下走！

还剩 ... 页未读，继续阅读 >>

免费阅读已结束，点击下载阅读编辑剩下 ... 页

阅读已结束，您可以下载文档离线阅读编辑

资源描述

HelsinkiUniversityofTechnologyDepartmentofComputerScienceDigitalSystemsLaboratoryOtaniemi,Otakaari1FIN02150ESPOO,FINLANDHELSINKIUNIVERSITYOFTECHNOLOGYDIGITALSYSTEMSLABORATORYSeriesA:ResearchReportsISSN07835396No.45;May1997ISBN9512236036MODELCHECKINGTHEBRANCHINGTIMETEMPORALLOGICCTLKeijoHeljankoDigitalSystemsLaboratoryDepartmentofComputerScienceHelsinkiUniversityofTechnologyOtaniemi,FINLANDHELSINKIUNIVERSITYOFTECHNOLOGYDIGITALSYSTEMSLABORATORYSeriesA:ResearchReportsISSN07835396No.45;May1997ISBN9512236036ModelCheckingtheBranchingTimeTemporalLogicCTLKeijoHeljankoAbstract:Reachabilityanalysisisamethodforanalyzingthedynamicbehaviorofaconcurrentsystem.OnewayofspecifyingthepropertiesthatthebehaviorsofthesystemmustfulllistousethebranchingtimetemporallogicCTL(Computationtreelogic).Theprocessofcheckingwhetherthebehaviorofthesystemfulllsthespeciedpropertyiscalledmodelchecking.InthisworkweanalyzeseveralalgorithmsforCTLmodelchecking.Themaincontributionofthisreportisanewmodelcheckingalgorithmwithtimecomplexitymatchingthebestexistingalgorithms,andmemoryrequirementswhichareeitherequalorsmallerthantheexistingalgorithms,dependingonthestructureofthesystemunderconsideration.Thealgorithmhasacounterexamplesandwitnessesfacility,whichisveryvaluablewhentryingtondthecauseofincorrectbehaviorofthesystem.Thepresentedalgorithmisalsostraightforwardtoimplementeciently,andwehaveimplementedthealgorithminthePRODtoolset.Keywords:Modelchecking,temporallogic,CTL,verication,reachabilityanalysis,state-spaceexploration,PRODPrinting:TKKMonistamo;Otaniemi1997HelsinkiUniversityofTechnologyPhone:90+35804511DepartmentofComputerScienceDigitalSystemsLaboratoryTelex:125161htkkOtaniemi,Otakaari1Telefax:+3580465077FIN02150ESPOO,FINLANDE-mail:lab@saturn.hut.Contents1Introduction12BranchingTimeTemporalLogic32.1BranchingTime...........................32.2TheBranchingTimeTemporalLogicCTL............72.2.1CounterexamplesandWitnesses.............112.3ASmallVericationExample...................123CTLModelChecking163.1TheSubformulaEvaluationOrder................163.2GlobalModelChecking......................193.2.1TheGeneralStructure...................193.2.2ANaiveImplementation..................233.2.3TheEMCModelCheckingAlgorithm..........263.3LocalModelChecking.......................304ANewGlobalModelCheckingAlgorithm444.1ModelCheckingtheUniversalUntilFormulas..........454.1.1SearchingforaCounterexample..............464.2ModelCheckingtheExistentialUntilFormulas.........494.2.1SearchingforaWitness..................514.3TimeandSpaceRequirements...................595ThePRODImplementation626Conclusions65References67AppendixA-MutexExamplePRODDescriptioniAppendixB-InitializationRoutinesii11IntroductionReachabilityanalysisismethodforanalyzingthedynamicbehaviorofacon-currentsystem.Thesystemisdescribedusingoneofthenumerousavailablemethodologies,forexample:concurrentprogramminglanguagessuchasSDL[24]andpromela[18],orPetri-Nets[14].Reachabilityanalysisthenprovidesawayofcreatingallthepossiblebehaviorsofthesystemstartingfromagiveninitialstate.Allthepossiblebehaviorsofthesysteminduceareacha-bilitygraph,whichisadirectedgraphinwhichthenodesareglobalstatesofthesystemandtheedgesareatomicstatetransitionsbetweenstates.Be-causereachabilitygraphgenerationiscompletelymechanicalitcanbeeasilyautomated,andgoodcomputertoolsupportisavailable.Thisthesisconcentratesonanautomatedmethodtoanalyzethecreatedreach-abilitygraphsusingatool.Theuserofthetoolcanofcourseinteractivelynavigatethereachabilitygraph,butthesheersizeofmanyreachabilitygraphsmakesndingerrorsinthiswayverydicult.Itiseasiertospecifytheprop-ertieswewantthereachabilitygraphtofulllusingsomeformalismandletthecomputerdothemechanicalchecking.Therehavebeenmanyad-hocwaysofdeningsuchpropertiesinthepast,butdierenttemporallogics[13]seemtobegettingwideacceptance.Intemporallogicweuselogicalformulastospecifypropertiesthatsomeorallofthebehaviorsofthesystemmustfulll.TheprocessofcheckingwhetheraformulaisTrueinaspeciedstateofthereachabilitygraphiscalledmodelchecking,anditcanbeautomatedwithatool.Inmanycasesititalsopossibleforthetooltogivefurtherinformationtohelptheusertondthecauseoferrorsinthesystem.Forexamplethetoolcangiveasequenceofstatesleadingtoastateinwhichthespeciedinvariantassertiondoesn’thold.InthisthesiswewillusethebranchingtimetemporallogicCTL(Computationtreelogic)[13]forspecifyingthepropertiesofsystems.WeareinterestedinthealgorithmsthatcanbeusedinmodelcheckingCTLformulas.ThebranchingtimetemporallogicCTLhasveryecientmodelcheckingalgorithms.Thebestalgorithmshaveworstcaserunningtimelinearbothinthesizeoftheformula,andthesizeofthereachabilitygraphi.e.O(length(f)(jSj+jRj)),inwhichthesizeofthereachabilitygraphisthesumofthenumberofstatesandtransitionsinthereachabilitygraph.ThiscomparesfavorablytothelineartimetemporallogicLTL[13],forwhichthemodelcheckingalgorithmscantakeexponentialtimeandspaceinthesizeoftheformulaintheworstcase.TheinitialgoalofthisworkwastoselectaCTLmodelcheckingalgorithmtobeimplementedinthePRODreachab