Exploration
MarshaChechikandArieGurfinkel
DepartmentofComputerScience,UniversityofToronto,
Toronto,ONM5S3G4,Canada.
Email:{chechik,arie}@cs.toronto.edu
Abstract.Model-checkingisbecominganacceptedtechniquefordebugginghardwareandsoftwaresystems.Debuggingisbasedonthe“Check/Analyze/Fix”loop:checkthesystemagainstadesiredproperty,producingacounterex-amplewhenthepropertyfailstohold;analyzethegeneratedcounterexampletolocatethesourceoftheerror;fixtheflawedartifact–thepropertyorthemodel.Thesuccessofmodel-checkingnon-trivialsystemscriticallydependsonmakingthisCheck/Analyze/Fixloopastightaspossible.Inthispaper,weconcentrateontheAnalyzepartofthedebuggingloop.Tothisend,wepresentaframeworkforgenerating,structuringandexploringcounterexampleseitherinteractivelyorwiththehelpofuser-specifiedstrategies.
1Introduction
Model-checkingisanautomatedverificationtechniquethatreceivesafinite-statede-scriptionofasystemandatemporallogicpropertyanddecideswhetherthepropertyholdsinthesystem.Model-checkingisrapidlybecominganacceptedtechniqueforanalyzingsoftwareandhardwaresystem.Inadditiontotellingtheuserwhetherthedesiredtemporalpropertyholds,itcanalsogenerateacounterexample,explainingthereasonwhythispropertyfailed.Typically,counterexamplesaregivenintermsofstatesandtransitionsofthemodelandcanbeeffectivelyusedfordebugging.Thecounterex-amplegenerationabilityhasbeenoneofthemajoradvantagesofmodel-checkingwhencomparedtootherverificationmethods.
Duringdebugging,amodel-checkerisusedasapartoftheCheck/Analyze/Fixloop:checkthemodel,analyzetheproducedcounterexample,fixthemodelortheprop-erty.Coptyetal.[7]describeseveralstagesofdebugging:(1)thespecificationdebug-gingstage,duringwhichwefixthepropertiestomakethemtrustworthy;(2)themodeldebuggingstage,duringwhichtheactualbugsinthemodelarebeingfound;and(3)thequalityassurancestagewhichaddressestheproblemof“regressionverification”–makingsurethatfixingoneerrordoesnotintroducenewones.
Counterexamplescanalsobeusedfordesignexploration[2].Amodel-checkeren-ablestheusertospecifyscenariosofinterestwithoutspecifyingtheexactinputse-quencesleadingtothem,andcanalsoreasonaboutmultipleexecutionsofthesysteminparallel.Thus,theusercanprovideasetofconstraintsintheformofatemporallogicpropertythatan“interesting”tracethroughthesystemshouldsatisfy,andthemodel-checkercomputessuchtraceswhilecheckingtheproperty.
Explainingwhyapropertypfailstohold(acounterexample)isthesameasex-plainingwhyaproperty¬pholds(awitness).Inthispaper,weoftenusewitnessesandcounterexamplesinterchangeably,referringtothemcollectivelyasevidence.
SomeversionoftheCheck/Analyze/Fixloopfrequentlyapplies,andthegoalofthisworkistomakethislooptighter.TheCheckphaseinvolvesrunningamodel-checker,whichisanexponentialalgorithmthatoftentakeshourstorunevenformoderately-sizedmodels[7].So,itisdesirabletominimizethenumberofmodel-checkingrunswhilemaximizingtheinformationobtainedfromeachrun.
TheAnalyzephaseismeasuredintermsofthetimethatanengineerspendsexplor-ingthegeneratedevidence,andthusiscostlyaswell.Itispossibleformodel-checkerstogeneratetoomuchevidence[9],floodingtheuserwithinformation,andmakingithardtobuildamentalpictureofwhatisgoingon.Inthiscase,theusermayspendtoomuchtimeandenergytryingtoreachtheportionofinterestorgetconfusedaboutthepurposeofagivensub-traceintheoverallexplanation.Also,sincethesizeofthepropertyunderanalysisistypicallymuchsmallerthanthesizeofthesystem,formula-specificpatternsoftenrepeatthemselvesthroughouttheevidence[9],andusersfailtonoticethem.Itisthereforedesirabletohavecontroloverjusthowmuchevidenceisgen-eratedbythemodel-checker.Thiscanbeaccomplishedviainteractiveexplanations–evidencegenerationbasedonuserpreferences.Interactiveexplanationscanallowuserstoputaboundonthetimethatthemodel-checkerspendscomputingtheevidence,andcontinueexploringitmanually;controlwhichoptionisusedtofacilitatethegenerationof“interesting”evidence;andcontroltheamountofinformationthatisgeneratedandpresentedbyrestrictingthescopeofexplorationaccordingtosomecriterionofinterest.Clearly,interactiveexplanationsmakestheproblemofgeneratingandunderstandingevidencetractable:
–Theamountofevidencegeneratedisbasedonwhattheuseriswillingtounder-stand.Thishelpsscalabilityofourapproachtolargemodels.
–Theamountofevidencedisplayedmakesiteasiertoidentify“interesting”casesandhelpswithdebugging.
Sincemodel-checkingrunsareexpensive,itisdesirabletoenableuserstofixasmanyerrorsaspossiblebeforerepeatingtheverification,ratherthaneliminatingonecounterexampleatatime.Forexample,wewouldliketoknowthatf∧gfailstoholdbecausebothfandgarefalse.Tothisend,providingtheuserwithalldisjointcounterexamplestoagivenpropertycansignificantlyshortenthedebuggingtime.Contributionsofthispaper.Inthispaper,weproposeaframeworkforstructuringandinteractivelyexploringevidence.Theframeworkisbasedontheideathatthemostgen-eraltypeofevidencetowhyapropertyholdsorfailstoholdisaproof.Suchproofscanbepresentedtotheuserintheformofproof-likecounterexamples[12]withoutsacri-ficinganyoftheintuitivenessandcloserelationtothemodelthatusershavelearnedtoexpectfrommodel-checkers.Basingtheevidenceonproofsallowsustounifyanum-berofexistingad-hocapproachestoexploringcounterexamples.Inparticular,notionsofforwardandbackwardexplorationaswellasstartingandstoppingconditionsarenaturalintheproofsetting.Proofscanalsobeusedtocontrolwhatkindofevidenceisbeinggenerated.Theprimarysourcesofsuchchoicesare:
1.determiningwhichpartofthepropertytoexplain(e.g.,ifthepropertyisp∨q,shouldthepresentedevidencebeforporforq?)and
2.determiningwhichpartofthemodeltousefortheexplanation(e.g.,ifthepropertyis“thereexistsanextstatewherepholds”andthemodelhasseveralsuchstates,whichshouldbepresented?).
Theabovechoicescanbemadebytheuserinteractivelyorautomatedintheformofstrategies(e.g.,iffacedwithachoiceofstatesfortheexplanation,alwayschoosetheonewheresomepredicatexholds).Theapplicationofstrategiesisimplementedinourframeworkbychangingtheproofrulesusedtogenerateevidence.Themodificationofproofrulescanbepermanentforthedurationoftheentirerunofthemodel-checker,andthuscanbefacilitatedbyhistory-freestrategies.Alternatively,theapplicationofstrategiescandependonthepreviously-observedbehaviourofthesystem.Forexample,toseetheinfinitealternationbetweenxandy,wemaywanttospecifyastrategythatoscillatesbetweenpreferringastatewherexholdsandastatewhereyholds.
Finally,fromthesoftwareengineeringpointofview,ourframeworkprovidesasimple,unifiedwaytointeractwiththecounterexamplegenerator.Theinteractionisbasedondefiningstrategiesthatcombineproperty-basedandmodel-basedchoices.Forexample,wecanspecifyastrategythatprefersthepartofthemodelthattheuserhasexploredpreviously,whileattemptingtosatisfyapartofthepropertyforwhichthewitnessistheshortest.
Clearly,mostuserscannotunderstandlargeproofs.Inourframework,proofsareusedintheback-end.Theyhelpgenerateandnavigatethroughtheevidence,withouttheneedtobepresentedtotheuser.Instead,usersseewitnessesandcounterexamples.Furthermore,largeproofsarenevercomputedinourapproachsinceprooffragmentsaregeneratedfromthemodel-checkingrunsaspartofinteractiveexplorationstofa-cilitateuser-understanding.Applicationofstrategiesfordynamicproofgenerationisthemajortechnicalcontributionofthispaper,whencomparedtoourpreviousworkreportedin[12].
Inthispaper,weillustratetheframeworkusingasimpleexampleratherthanval-idatingitseffectivenessviaasizablecasestudy.Here,wedrawonindustrialexperi-ence[7]thatbeingabletolimittheamountofevidenceshownandgeneratingseveralcounterexamplesatonceisextremelyeffectiveinreducingtheeffortthatengineersspendlookingforarealcauseofanerror.Ourframeworkunifiesanumberofexistingapproachesandallowsuserstocreateadditionalstrategiesthatmayfurtherimprovethedebuggingprocess.Thus,itcanbeusedforexplainingthereasonwhytheprop-ertyfailedorsucceeded,determiningwhetherthepropertywascorrect(“specificationdebugging”),andforgeneralmodelexploration.
RelatedWork.Theproblemofgeneratingandanalyzingcounterexamplesformodel-checkingcanbedividedintothreecategories:generatingthecounterexampleefficiently,obtainingavisualpresentationsuitableforinteractiveexploration,andautomaticallyanalyzingthecounterexampletoextracttheexactsourceoftheerror.
Theoriginalcounterexamplegenerationalgorithm,implementedinmostsymbolicmodel-checkers,wasproposedbyClarkeetal.[5],andwaslaterextendedtohandlearbitraryuniversalproperties[6,12],i.e.,propertiesthatquantifyoverallpathsofthemodel.AnalternativeapproachwasindependentlysuggestedbyNamjoshi[13]andTanandCleaveland[16]withthegoaltoextendthecounterexamplegenerationtech-niquetoall(asopposedtojustuniversal)branchingtemporalproperties.Theproposedmethodsidentifywhatinformationmustbestoredfromtheintermediaterunofthemodel-checkertoreconstructtheproofofcorrectnessoftheresult.AsimilartechniqueforlinearpropertieswasexploredbyPeledetal.[14].
TheproblemofthevisualpresentationofgeneratedcounterexampleswasaddressedbyDongetal.[9,8].Theauthorsdevelopedatoolthatsimplifiesthecounterexampleexplorationbypresentingevidencethroughvariousgraphicalviews.Inparticular,theyfoundthatoneofthemostimportantpartsofthevisualizationprocessishighlightingthecorrespondencebetweentheanalyzedpropertyandthegeneratedcounterexample.
Theproblemoftheautomaticanalysisofcounterexampleswasaddressedbymanyresearchersbutspacelimitationsdonotallowustosurveythemhere.Manyofthesetechniques(e.g.[11,1])arebasedoncomparingallcounterexamplestoasafetyprop-erty(i.e.,atemporalpropertywhereacounterexamplehasafinitenumberofsteps)toidentifythecommoncauseoftheerror.
Thegoalofourworkistodevelopaunifyingframeworkforcombiningvariousvisualizationandanalysistechniques.Inthat,theworkofCoptyetal.[7]istheclosesttoours.Theauthorsreportona“counterexamplewizard”–atoolforcounterexam-pleexplorationforsafetyproperties.Thekeyideaoftheapproachistocomputeandcompactlystoreallcounterexamplestoagivenproperty.Userscanthenvisualizetheresultinvariousways,replayseveralcounterexamplesinparallel,andapplydifferentautomaticanalysistechniques.
Organization.Therestofthispaperisorganizedasfollows:WediscussCTLmodel-checkinginSection2andtheframeworkfromtheuserperspectiveinSection3.InSection4,wediscusstheinternalsoftheframework.InSection5,weenrichtheframe-workwithadditionalproofstrategiesthatallowtheusertocontrolwhichcounterex-amplegetsgenerated.InSection6,wediscusshowtouseourframeworktogenerateseveralcounterexamplesatonce.WeconcludeinSection7withthesummaryofthepaperanddiscussionoffutureresearchdirections.AppendixAdescribesKEGVis–aprototypeimplementationofourframework.
2CTLModel-Checking
Model-checkingisanautomatedverificationtechniquethatreceivesasystemKandatemporallogicpropertyϕanddecideswhetherϕholdsinK.Inthispaper,weassumethatKisaKripkestructureconsistingofafinitesetofstatesS,adesignatedinitialstates0,asetofatomicpropositionsA,atotaltransitionrelationR⊆S×S,andalabelingfunctionI:S→2Athatassignsatruthvaluetoeachatomicpropositionineachstate.AnexampleKripkestructureisshowninFigure1(a).
WespecifypropertiesinComputationTreeLogic(CTL)[4],definedbelow:
ϕ=a|ϕ∨ϕ|ϕ∧ϕ|¬ϕ|EXϕ|AXϕ|EFϕ|AFϕ|EGϕ|AGϕ|E[ϕUϕ]|A[ϕUϕ]
whereaisanatomicproposition.Themeaningofthetemporaloperatorsis:givenastateandpathsemanatingfromit,ϕholdsinone(EX)orall(AX)nextstates;ϕholdsinsomefuturestatealongone(EF)orall(AF)paths,ϕholdsgloballyalongone(EG)orall(AG)paths,andϕholdsuntilapointwhereψholdsalongone(EU)orall(AU)paths.SomepropertiesofthemodelinFigure1(a)are:“itispossibletogeneratearequest”(EFr)and“onceabuttonispressed,arequestwillbegenerated”(AG(p⇒AFr)).
Wewrite[[ϕ]]K(s)toindicatethevalueofϕinthestatesofK,and[[ϕ]](s)whenKisclearfromthecontext.AformulaϕissatisfiedinaKripkestructureKifandonlyifitissatisfiedinitsinitialstate.TheoperatorsEX,EG,andEUformanadequateset,
s2s0s1pprs4prfs0s6pfs1ps3rs3rs5rffs7pprs0s1s2Fig.1.(a)StatemachineforthemoduleButton;(b)Twowitnessesoflength3for[[EFr]](s0)forthisstatemachine.
AXϕ¬EX¬ϕAFϕA[trueUϕ]E[ϕU0ψ]ψEFϕE[trueUϕ]AGϕ¬EF¬ϕE[ϕUiψ]ψ∨(ϕ∧EXE[ϕUi−1ψ])
A[ϕUψ]¬E[¬ψU¬ϕ∧¬ψ]∧¬EG¬ψ
Fig.2.DefinitionsofCTLoperators.
i.e.allotheroperatorscanbedefinedfromthem,asshowninFigure2.SemanticsEX,EGandEUisformallyindefinedasfollows:
[[EXϕ]](s)iff∃t∈S·R(s,t)∧[[ϕ]](t)
[[E[ϕUψ]]](s)iffthereexistsapaths0,...,snsuchthats=s0and[[ψ]](sn)and∀i 3UserViewofTheFramework Inthissection,weillustratetheframeworkfromtheuserperspectiveonafamiliarexampleofanelevatorcontrollersystem. 3.1ElevatorControllerSystem Anelevatorcontrollersystemconsistsofasingleelevatorwhichacceptsrequestsmadebyuserspressingbuttonsatthefloorlandingsorinsidetheelevator.Theelevatormovesupanddownbetweenfloorsandopensandclosesitsdoorsinresponsetotheserequests. WeusethemodelspecifiedinSMVbyPlath&Ryan[15].Wedonotpresentthestate-machinemodelherebecausethepurposeofouruseofcounterexamplesismodeldebuggingandmodelunderstanding.However,toillustrateafewconcepts,wedopro-videastatemachineforamoduleButton,showninFigure1(a).OneinstanceoftheButtonmoduleisproducedforeachbuttoninsidetheelevatorandonfloorlandings. Variablefdetermineswhentherequesthasbeenfulfilledandthebuttoncanbereset.Wemodelthelatchingexplicitly:variablepdeterminesthestateofthebutton(pressedorreleased),whereasrdetermineswhethertherequesttomovetothedesiredfloorhasbeengenerated.Wefurtherassumethatarequestcannotbefulfilledbeforeithasbeengenerated,i.e.,fcannotbecometrueifrisfalse.InFigure1(a),weonlyshowtruevariables;thus,instates0,p,r,andfarefalse. 3.2WitnessesandCounterexamples SupposeweareinterestedincheckingthefollowingpropertyoftheButtonmodule:“itisneverthecasethatarequestcanbefulfilled”,expressedinCTLasAG¬f.The sssss(a)(b)(c)Fig.3.PossiblewitnessesforEGpinstates:(a)aloopingwitness,(b)apathfollowedbyaloop,and(c)twowitnessescombiningcases(a)and(b). counterexampletothispropertyisafinitepaththatstartsintheinitialstate(s0)andarrivesatthestatewherefistrue,e.g.,s0,s1,s2,s5.Notethatthispathisalsoawitnesstothenegationoftheaboveproperty:EFf,i.e.,“itispossibletofulfillarequest”. Consideranotherproperty:“wheneverarequestisgenerated,itwilleventuallybefulfilled”,formalizedinCTLasAG(r⇒AFf).Thecounterexampletothisproperty,orawitnesstotheequivalentpropertyEF(r∧EG¬f),isaninfinitebehaviorthatdescribes(1)howthesystemcanreachastatewhererholdsandfromthenon(2)howitcanavoidenteringastateinwhichfholds.Onesuchpathiss0,s1,s2(reachingr),followedbyaloopats2(sofisalwaysfalse). Unliketraditionalmodelcheckers,ourframeworkdoesnotautomaticallygenerateasinglecounterexample.Instead,itautomatestheprocessofdynamicallyconstructingone,orseveral,startingfromtheinitialstate.Further,itgivestwoseparateviewsofthecounterexample:thelow-levelview,whichdescribeseachstateexplicitly,namingitsvariables,andahigh-levelviewthatshowsthecompletetraceandannotateseachstatewithadditionalinformation,whichwerefertoassummaries,describingthesignificanceofthestatewithrespecttotheoverallproperty,andsummarizingtherestofthetrace.3.3ExploringtheElevatorControllerModel WenowdescribeuserinteractionswiththeframeworkwhiledebuggingandexploringtheElevatormodel. Generatingseveralcounterexamplesatonce.Whenwestartverifyingthesystemusingthemodel-checker,itisusuallythecasethatthepropertywearetryingtocheckiswrong.Considertheproperty:“fromanystate,allpathsgothroughastatewheretheelevatorisonthethirdflooranddoorsareopen”(AGAF(floor=3∧doors=open)).Thefirstcounterexampletellsusthatitispossibletostartonthefirstfloorandstaythereforever.Wemayconcludethatthefirstflooris“special”,andinsteadcheckthatourdesiredconfigurationisreachablefromanyfloorexceptthefirstone:AG(floor=1⇒AF(floor=3∧doors=open)).Thecounterexamplewegetinthiscasewouldleadustothesecondfloorandremainthereforever,orpossiblyoscillatebetweenthefirstandthesecondfloor,withouteverreachingthethird.Seeingallthreecounterexamplesatoncewouldhavehelpedusdeterminethattheelevatornevergetstothethirdfloorunlessarequestforthisfloorhasbeenmade,andthepropertyshouldhavebeenupdatedtoAG(btn3.r⇒AF(floor=3∧door=open)). Excludingaknowncounterexampleviastrategies.Considertheaboveexample.In-steadofmodifyingthepropertytoexcludeourfirstcounterexample,whichisoftendifficultforengineers,wespecifyastrategythatattemptstoavoidthestatewherefloor=1,ifpossible.Asuccessofthisstrategyallowsustodiscoverfurthercoun-terexampleswithoutmodifyingtheproperty. Preferring/avoidingtheexploredpartofthemodel.Ourmodeloftheelevatorcon-trollercomeswithanumberofdesiredproperties,e.g.,“theelevatornevermoveswithitsdoorsopen”,“everyrequestfortheelevatoriseventuallyfulfilled”,etc.Whenana-lyzingafewofthese,wequicklygetfamiliarwithpartofthemodel,e.g.,wediscover thattheelevatorcanstayinastatewherefloor=1,doorsareclosed,thestateofthecontrollerisnotMoving,andthedirectionoftheelevatorisup.WecallthisstateIdle. Strategiesallowengineerstousetheirknowledgeof“designated”states,suchasIdle,toguidethecounterexamplegeneratortowardstheminthecasewhereanAFpropertyisfalse.Inparticular,usingtheinformationaboutthestateofthedoors,thedirectionofthemovement,andthestateofthecontroller,wedefineadistancefunctionbetweentheIdlestateandthecurrentstateofthemodelandspecifyastrategythatpicksastatewherethisdistanceisminimized. Notethatanadditionalbenefitofusingthisstrategyduringdebuggingisthatwecanstaywithinabetter-understoodpartofthemodel.Ontheotherhand,ifthegoalofmodel-checkingismodelexploration[2],wemayinsteadchoosetoavoidtheknownbehaviorbymaximizingthedistancebetweenthenextstateintheproofandIdle.Choosingthe“best”loopusingsummaries.GeneratingtheshortestcounterexampleforanarbitrarytemporalpropertyisNP-hard[5],andthusconventionalmodel-checkersapplyagreedystrategybycomputingtheshortestcounterexampletoeachsubformula.InthecaseofcounterexamplestoAFp(orwitnessestoEG¬p),eventhisstrategyishardtoimplement.Instead,model-checkersconsiderastatestosatisfyEGpifeitherthereisapathonwhichpholdsineachstatethatloopsarounds(seeFigure3(a))orthereisasuccessorofsinwhichpholdsandthereisaloopingpathofp-statesaroundit(seeFigure3(b)).Thus,thealgorithmtocomputeawitnesstoEGpinstatescheckswhetherthereisapaththatleadsbacktosandonwhichpholdsineachstate,terminatesifsuchapathisfound,andotherwisepicksasuccessorofswhereEGpholdsasthenewstateandcontinues.Suchanalgorithmpicksthefirstlooponapath,evenifitislongandhardtoexplore.WeillustratethisscenarioinFigure3(c):thedashedlooparoundsmaybeshortandsimple,whereasconventionalmodel-checkersalwaysreturnthesolidlooparounds,ifoneexists,asthewitnesstoEGp. Ourframeworkallowstheusertodefinestrategiestolooparoundafamiliarstate(e.g.,Idle)orusestatesummariestochoosethemostinterestingloop.ConsiderthewitnesstoapropertyEGpinthestates1ofthemodelinFigure1(a).Clearly,thereareseveralpathsthatsatisfyit:s1,followedbyalooparounds2;aloops1,s2,s4,s1;aloops1,s2,s4,s6,s1,etc.Theframeworkdisplaysthestates1andindicatesthatEGpholdsinit;thisisthecurrent“explanation”ofthestates1.ClickingonEGpproducesfurtherexplanationsofwhyEGpholdsins1:(1)s1ispartofathree-stateloopandpholdsineachstateoftheloop;(2)thereisasuccessorstateofs1fromwhichwecanexplainEGp.Clickingonthesecondexplanationtellsusthatthesuccessorstateofinterestiss2,andEGpholdsinit.ClickingonthisEGptellsusthereason:(2a):thereisaself-loop(aloopoflength0)arounds2andpholdsins2;(2b):thereisasuccessorstateofs2inwhichEGpholds.Atthispoint,wecaneithergobacktothefirstexplanationandinafewclicksrevealthethreestatesoftheloop,ordecidethattheself-looparounds2providesthebetterexplanation.Ofcourse,wecancontinuelookingforotherexplanationsuntilallpossiblep-loopshavebeendiscovered. Alternatively,afterthefirstexplanationthattellsusthats1ispartofathree-stateloop,wemaychoosetodefineastrategythatexaminesthemodelfromstates1uptodepththreetoseewhetherthereareotherwitnessestoEGpandhowlongthecorre-spondingloopsare,andthenchoosestheshortestsuchlooptoexplore. Proofstrategiesproof rules for temporal logicproof rules for prop. logicaxioms of the modelaxioms of Kripke structuresBasic proofstrategyDatabase ofproof rulesModelProof keeperPropertyModel checkercounterexample(evidence)Visualization engineVisualizationstrategiesFig.4.Overviewoftheframework. ab [[EXϕ]](s) ∨-rule ∃n·[[E[ϕUnψ]]](s) ∃x∈D·f(x)EUiEX [[ψ]](s) a∨bb one-pointrule [[E[ϕUnψ]]](s) Fig.5.SomeCTLproofrules. 4Framework TheframeworkforgeneratingandvisualizingcounterexamplesisshowninFigure4.Dashedlinesindicateoptionalinputs.TheuserinteractionwiththeframeworkstartsbyprovidingaproofkeeperwithamodelKandapropertyϕ.Theproofkeeperisthecentralpartoftheframework,responsibleforgenerating(afragmentof)theproofandpresentingittotheuser.First,itcallsamodel-checkertofindoutwhetherϕissatisfiedorviolatedbythemodel.Itthenusesthedatabaseofproofrules,accordingtoauser-specifiedproofstrategy,toprovethatfact.Inthisstep,itusesthemodel-checkertodecidewhichproofrulesareapplicableandtoensurethesoundnessoftheproof.(Additionalrunsofthemodel-checkercanbeavoidedbyefficientlycomputingandstoringevidence,asdiscussedin[16,13,12].)Thecurrentprooffragmentproducedbytheproofkeeperisshowntotheuserviaavisualizationengine.Theinteractionoftheuserwiththispartoftheframeworkiscapturedbyuser-suppliedvisualizationstrategies.Intherestofthissectionwediscusstheframeworkinmoredetail.TheframeworkaugmentedwithadditionalproofstrategiesisdescribedinSection5.4.1ProofRules SeveralproofrulesfromtheCTLproofsystemaregiveninFigure5.Theseincludeallproofrulesofthepropositionallogicthatdealwithdisjunctionandconjunction,suchasthe∧-,∨-rules,i.e.,toprovea∧b,weneedtoproveaandbseparately,andtoprovea∨b,weneedtoproveeitheraorb.Additionally,ourproofsystemusestheaxiomatizationofthegivenKripkestructureK,describingitstransitionrelationRandvaluesofeachatomicpropositionineachstate.Forexample,someoftheaxiomsofthemodelinFigure1(a)are:thereisatransitionbetweens0ands1(R(s0,s1));thereisnotransitionbetweens0ands3(¬R(s0,s3));pistrueins1(I(s1,p)),etc. Theproofsystemisthenextendedwithproofrulesforeachtemporaloperator.Inthispaper,weonlyshowproofrulesforEXandEU,andreferthereaderto[12]fora [[r]](s2) R(s1,s2) R(s0,s1) [[EX(f∨r)]](s1) EUi EX [[f∨r]](s2) ∃t·R(s1,t)∧[[f∨r]](t) [[E[U2(f∨r)]]](s0) [[E[U(f∨r)]]](s0) EU [[E[U2f∨r]]](s0) thebehaviorofthemodelthatisusedtojustifytheresultofthemodel-checker.Thisisachievedbyextractingthesetofmodelexecutiontracesfromtheproof,andlabel-ingeachstateofthetracewiththepartoftheproofthatdependsonit.Forexample,aproof-likewitnessfortheproperty[[EF(f∨r)]](s0)isshowninFigure6(b).Thispropertyiswitnessedbya3-statepaths0,s1ands2.Theproofinstates0tellsusthatastateinwhichf∨rholdsisreachableinexactlytwosteps,sincetheEFoperatorisexplainedbyanEUwiththebound2.Inthelaststepoftheproofinstates0,thedottedarrowconnectingtheformulaEXEX(f∨r)andthestates1,tellsusthats1isthewitnessfortheoutermostEXoperator.Theproofattachedtostates2tellsusthattheformulaf∨rholdsinitbecauseristrue. Thepartsoftheproofattachedtoeachstatecanbeseenassummariesthatexplainwhatisgoingtofollow.Forexample,theproofattachedtothestates0inFigure6(b)canbesummarizedas“thenextstateisanintermediateone,andthenwereachthedesiredstate”.Othertypesofsummariesindicatewhetheragivenstateispartofaloop,whichpartofthepropertyisbeingexplained,etc. Thevisualpresentationoftheresultiscontrolledbytheuserthroughvisualiza-tionstrategies.Atypicalstrategyistorestrictthescopeoftheexplanationinordertobringforwarditsmostusefulparts.Thisisaccomplishedbyspecifyingastartingandastoppingconditionforthevisualization.Forexample,torestrictthewitnessoftheprop-ertyϕ=EGEF(x∧EXx)totheEFoperator,wesetthestartingandthestoppingconditionstoEF(x∧EXx)andx∧EXx,respectively.Intheproof-likewitnessinFigure6(b),specifyingthatf∨risthestoppingconditionremovestheproofattachedtothestates2.Ifweletf∨rbethestartingconditioninstead,s2wouldbetheonlydisplayedpartofthewitness. Avisualizationstrategycanalsocontrolhowthestateinformationispresented.Forexample,wecanrequesttoshowallvariablesineachstate,refertoeachstatebyauniquename(asinFigure6(b)),showonlythosevariablesthatchangebetweenstates,oralwaysdisplaysomespecificvariables.Furthermore,thestrategycancontroltheverbosityoftheproofannotations,orcompletelyreplacetheactualproofwithamoresuitableexplanation.Forexample,wecanreplacetheproofattachedtothestates0withits(English)summary. Theresultcanbeexaminedinatraditionalforwardfashion–startingfromtheinitialstateandproceedinginthedirectionofthetraceexecutiontoanerrorcondition.Alternatively,theusercanstarttheexplorationattheerrorconditionandusetheproofannotationstomovebackwardsalongthetrace.Thiscorrespondstoconstructingtheproofofthepropertyfromthebasicaxiomsofthesystem. Thevisualizationenginethatwepresentedinthissectionenablesusersfamiliarwithmodel-checkingtodefinestrategiesforcounterexamplegenerationandexploration.Italsoallowsuserswhoarecomfortablewithsimpleproofstosearchthroughthecoun-terexampleeffectivelyusingtheproofview.Yet,itisverysimplistic–itisvirtuallyaback-endvisualizer.Tobeuseful,ourvisualizationenginemustbeextendedwithadditionalvisualcues,e.g.,assuggestedin[9,8](seeSection7). 5AddingUser-SpecifiedStrategies Theabilityofausertounderstandwhydesiredpropertiesholdorfailinthemodelcanbegreatlyenhancediftheusercancontrolthekindofevidencethatgetsgeneratedas partoftheexplanation.Thisapproachalsomakesproofgenerationmuchmorescalable:onlythefragmentoftheproofthattheuserwantstoseegetsgeneratedanddisplayed. ConsidertheexampleinFigure6.Thepresentedwitnessgoesthroughthestates2oftheKripkestructureinFigure1(a),whereastheusermayhavepreferredittogothroughs3instead.Thisisamodel-baseddecisionthatcomesfromthefactthatseveralstatesmaysatisfy[[EXϕ]](s1),forsomepropertyϕ.Theusercanchoosewhichofthese(orwhetherallofthese)areusedintheproof. Theseconddecisiontypecomesfromexplicitchoicesinproperties,viaadisjunc-tionoperator,e.g.,[[EFp∨EGr]](s3).Ifbothdisjunctsaretrue,asinthemodelinFigure1(a),theproofofwhichdisjunctshouldbeshown?Controllingthisisespeciallyusefulduringthespecificationdebuggingphaseoftheverification. Typically,aproofproceedsbydecomposingthetop-levelgoalintosimplersub-goals.Forexample,toprove[[p∧r]](s2),weneedtoprove[[p]](s2)and[[r]](s2)sepa-rately.Yet,iftheaimofgeneratingtheproofisdebugging,wecanoftenfindthesourceoftheerrorwithoutexpandingallofthesubgoals.Thechoiceoftheorderinwhichsubgoalsaretobeexpandedisthethirdtypeofdecisionthattheusermaywanttomakewhengeneratingproofs.WegivethepseudocodeoftheproofgenerationinthemethodbuildProof(),showninFigure7(a).Thebasicproofstrategy,describedinSection4andshowninFigure7(c),makesallchoicesatrandom.Userscanaffecttheproofgenerationbycreatingotherstrategies. Thesimplestformofastrategyistostopandasktheusertochooseeverytimeadecisionneedstobemade.Userscanbeaidedinmakingdecisionsbyproofsummariesgeneratedbythemodel-checker.Forexample,whenchoosingthepartoftheformula[[EFp∨EGr]](s3)toexpand,theusermaywanttonotethat[[EFp]](s3)convergedinoneiterationand[[EGr]](s3)convergedintwo,andthuspick[[EFp]](s3).Strategiescanalsobeautomated,withdecisionsbasedonsummaries,observedhistoryoftheex-ecution,orotheruserpreferences.Inthissection,wediscussvarioustypesofstrategiesandtheirsupportinourframework. 5.1SpecifyingStrategies Auser-specifiedstrategyiscreatedbyimplementingtheStrategyinterfaceshowninFigure7(b).Inparticular,thestrategycanmodifythedefaultproofsystembeforetheproofgenerationbeginsusinginit(),determinewhichsubgoalistobeexpandedusingpickLeaf(),anddeterminewhichruleoutoftheapplicableonesistobeappliedusingpickRule().Finally,aftertheapplicationofanyproofrule,thestrategycanexecuteitsownruleAppliedmethod.Inaddition,strategieshavefullaccesstotheproofsystem:theycanexaminethecurrentproof,addorremoveproofrules,andexaminetheresultofanyruleapplication.Thus,theycanaffectthebehaviouroftheproverbasedonthecurrentsubgoal,proofrulesthathavealreadybeenapplied,otherhistoricalinformation,subgoalsyettobeproven,etc. Wenowdemonstratehowafewusefulstrategiescanbespecifiedinourframework.Choosingthesmallestsubgoal.Thegoalofthisstrategyistoalwayspickarulethatresultsinasubgoalwiththeleastnumberoftemporaloperators.Forexample,supposeourcurrentsubgoalis[[p∨EFq]](s),andtherearetwoapplicableproofrulesfordis-junction(seerulesQ1Figure8(a),(b)).Clearly,applyingruleQ1resultsinashorterproof,andthereforeashorterwitness.Animplementationofthisstrategyisshownin 1:voidbuildProof(Strategyst)2:st.init() 3:repeatuntilleaves=∅ (a)4: l=st.pickLeaf(leaves)5:r=st.pickRule(getRules(l),l)6:result=apply(r,l)7:st.ruleApplied(r,l,result)8:endrepeat1:classBasicStrategyextendsStrategy2:NodepickLeaf(Setleaves) (c)3: returnrandomElmnt(leaves)4:RulepickRule(Setrules,Nodel)5:returnrandomElmnt(rules) 1:classPickExploredextendsStrategy2:voidinit()3:N=s0 4:addRule([[EXϕ∧N]](s) (e) [EFq]](s) [[p∨EFq]](s)Q[1 B⇒p [[ϕ∨ψ]](B) 1:classStrategy 2:voidinit() 3:NodepickLeaf(Setleaves) (b)4:RulepickRule(Setrules,Nodel) 5:voidruleApplied(Ruler,Noden,Noder)1:classPickDisjunctextendsStrategy2:RulepickRule(Setrules,Nodel)(d)3:pickQinruless.t.4:size(tryApply(Q,l))isminimal [[EXϕ]](s)Q1) 4:addRule( [[EXϕ∧c2]](s) state=true 6:RulepickRule(Setrules,Nodel)7: ifc1 state=false10:returnQ111:endif12:else 13:ifQ2∈rulesthen14: c1 [[EXϕ]](s) EXc ∨-rule ∃B1·R(B,B1)∧[[ϕ]](B1) Sequentialconstraint.Thegoalofthisstrategyistoensurethatstatesthatsatisfysomeconditionc1alternatewithstatesthatsatisfyanotherconditionc2oneverypathofthewitness.AswiththePickExploredstrategy,itbeginsbyaddingnewproofrulesfortheEXoperator.ItspickRulemethodusesanadditionalbooleanvariablec1 r∧¬f⇒r R(s1,{s2,s3}) R(s0,s1) [[EXr]](s1) [[EFr]](s0) Fig.9.Proofof[[EFr]](s0)forthemodelinFigure1(a). valueofpbetweenstatess2ands3,andthuspisnotpartoftheformuladescribingthethirdstate. Propositionalformulasprovideaverycompactpresentationofallofthewitnessesatonce,whichinturnhelpsfocustheattentionoftheusertothemorerelevantpartsoftheexplanation.Forexample,byexaminingtheconstraintofthethirdstate,weseethatthevalueofpisirrelevant.In[7],itwasshownthatsuchapresentationcandramaticallyreducethetimerequiredbytheengineerstolocatetherealcauseofanerror. Intherestofthissection,weshowthatourframeworkcanbeusedtogenerateabstractwitnessesforreachabilityproperties,orequivalently,abstractcounterexamplesforsafetyproperties.AnyreachabilitypropertycanbeexpressedusingacombinationofEX,andEUoperatorsandpropositionalconnectives[4].Toconstructaproofthatcapturesallwitnessesatonce,weneedtoextendthecorrespondingproof-rulesfromsinglestatestosetsofstates. Fornotationalconvenience,wewrite[[ϕ]](B)tostandfor∀s∈B·[[ϕ]](s),whereϕisatemporallogicformula,andBisasetofstates.Furthermore,weextendthetransitionrelationRtosetsofstatesandwriteR(B,C)tostandfor∀b∈B·∃c∈C·R(b,c).ToprovethatapropositionalformulapholdsinallstatesofasetB(writtenas[[p]](B)),weneedtoshowthatBisasubsetofthesetofstatesdefinedbytheformulap.Thatis,piscompatiblewiththepropositionalconstraintsimposedbyB.Formally,weobtaintheatomic-rule,showninFigure8.Forexample,thefactthatrholdsinthesetofstates{s2,s3}oftheButtonmodulefollowsfromtherelation(r∧¬f)⇒r.Toprovethatϕ∨ψholdsinasetofstatesB,weneedtoshowthatthereexistsapartitioningofBintosetsB1andB2,suchthatϕholdsinallelementsofB1,andψholdsinallelementsofB2.Theaboveiscapturedbythe∨-rule,showninFigure8.Notethatuser-specifiedstrategiescaninfluencethechoiceofthispartitioning.Forexample,ifapropertyϕismorecomplicatedthanψ,theusermaypreferB1tobeempty,ifpossible. ToprovethatEXϕholdsinasetofstatesB,weneedtoidentifythesuccessorstatesofeachstateinBandprovethatϕholdsinthem(seetheEXruleinFigure8).Inpractice,thesetB1canbeeasilycomputedfromtheintermediateresultsofasymbolicmodel-checker.Forexample,itcanbeinstantiatedtothesetofallstatesthatsatisfyϕ,andthataresuccessorsofstatesinB.Onceagain,theusercancontroltheexactchoiceofB1usingaproof-strategy,wherepickingthelargestsuchsetleadstoanabstractwitnesscapturingallpossiblewitnesses. RecallfromSection4.1thatproof-rulesfortheEUoperatorarederivedbyreducingittoaformulacontainingadisjunction,aconjunction,andanEXoperator.Thus,itcanbetriviallyextendedtosetsofstatesusingtherulesdefinedinthissection. Asampleproofproducedviatheaboveproofrulesfortheproperty[[EFr]](s0)evaluatedintheButtonmodule,isshowninFigure9.Thisproofcapturesall3-stepwitnessesforthisproperty. 7Conclusion Inthispaper,wepresentedageneralframeworkforgeneratingandexploringwitnessesandcounterexamplesoftemporallogicproperties.Theframeworkisbasedonbuildingevidenceintheformofaproofandcontrollingwhichportionsoftheproofareexpandedandshowntotheusereitherinteractivelyorviauser-specifiedstrategies.Proofsalsofacilitateeasygenerationofconventionalwitnesses,whichinourcaseareaugmentedwithsummariesdescribingwhichpartofthepropertyisbeingexplained,whetheragivenstateispartofaloop,howmanystepsseparateagivenstatefromtheoneinwhichasubpropertybecomestrue,etc.WehavealsocreatedKEGVis–aprototypeimplementationoftheframework. Wearecurrentlylookingatwaystoconnectexplorationstrategieswithtemporallogicpropertypatterns[10].Further,ourpreliminaryexperiencewithKEGVisindicatesthatusersoftenmakesimilarchoicesduringtheirinteractiveexplorationofwitnesses.Anautomatedstrategyassistantthatattemptstolearnuserpreferencesfrompreviousinteractionswiththesystemandsuggestanappropriatestrategywouldgreatlyenhancethepotentialusabilityofourframework.Finally,weareinterestedinhowstrategiescanbeusedforunderstandingtheimpactofchangingamodel. Weviewourcurrentimplementationasaback-endforasuccessfulevidenceexplo-rationtooland,initscurrentform,itisbynomeansreadytobeappliedinanindustrialsetting.Toenablesuchanapplication,thetoolmustbecomemuchmoreuser-friendly.Mostengineersfindproofstoodifficult,and,althoughproof-likewitnessesbridgethegapbetweenproofsandmodels,theconceptofaproofiscurrentlycentraltonodesummariesandsomepartsofthemanualexploration. Forthesakeofgenerality,ourworkhasbeenonthelevelofthelowestcommondenominatoroftheinteractionbetweentheuserandthemodel-checker.Namely,weassumedthatthemodelofthesystemisgivenbyaKripkestructure,andpropertiesofinterestarespecifieddirectlyintemporallogic.Thismakesitpossibletoeasilycombineourapproachwithmanyoftheexistingmodel-checkingtools.However,thisalsomakestheactualtechniqueappearmorecomplexthanitreallyis. Forexample,insoftwaremodel-checking,theuserinteractswithamodel-checkerbyprovidingasourcecodeoftheprogram,andthemodel-checkerautomaticallyex-tractsaKripkestructurefromit.Clearly,inthiscase,itisnothelpfultoexplaintheresultofthemodel-checkingrunusingstatesofthisKripkestructure.Instead,suchstatesshouldbeconvertedbacktowhattheyaremeanttorepresent,namely,linenum-bersoftheprogramandvaluesofrelevantvariables.Furthermore,sequencesofstatescanbeconvenientlypresentedviainteractivedebugsessions.Theproofpartoftheex-planationisstillusefulinsuchcases:itcanbeusedtoannotatethedebugtrace,e.g.,toexplainwhyaparticularbranchoftheprogramistakennext,orthatthemodel-checkerdiscoveredanon-terminatingloopintheprogram.Presentationofmanyofsuchproofaspectscanalsobetailoredtoaparticulardomain.Forexample,“anerrorin3steps”canbecomeagraphicaliconintheannotationofthetrace. Overall,wefeelthatthepresentedframeworkisflexibleenoughtoenablecreationoftrulyuser-friendlytoolsthatcanfacilitateeffectivemodelexplorationanddebuggingusingmodel-checkingtechnology. References 1.T.Ball,A.Podelski,andS.Rajamani.“BooleanandCartesianAbstractionforModelCheck-ingCPrograms”.STTT,5(1):49–58,November2003. 2.S.Barner,S.Ben-David,A.Gringauze,B.Sterin,andY.Wolfsthal.“AnAlgorithmicAp-proachtoDesignExploration”.InProceedingsofFME’02,volume2391ofLNCS,pages146–162.Springer-Verlag,July2002. 3.M.Chechik,B.Devereux,andA.Gurfinkel.“χChek:AMulti-ValuedModel-Checker”.InProceedingsofCAV’02,volume2404ofLNCS,pages505–509,July2002.4.E.Clarke,O.Grumberg,andD.Peled.ModelChecking.MITPress,1999. 5.E.M.Clarke,O.Grumberg,K.L.McMillan,andX.Zhao.“EfficientGenerationofCoun-terexamplesandWitnessesinSymbolicModelChecking”.InProceedingsofDAC95,pages427–432,1995. 6.E.M.Clarke,Y.Lu,S.Jha,andH.Veith.Tree-LikeCounterexamplesinModelChecking.InProceedingsofLICS’02,pages19–29,July2002. 7.F.Copty,A.Irron,O.Weissberg,N.Kropp,andG.Kamhi.“EfficientDebugginginaFormalVerificationEnvironment”.InProceedingsofCHARME’01,volume2144ofLNCS,pages275–292.Springer-Verlag,September2001. 8.Y.Dong,C.R.Ramakrishnan,andS.A.Smolka.“EvidenceExplorer:AToolforExploringModel-CheckingProofs”.InProceedingsofCAV’03,volume2725ofLNCS,pages215–218,2003. 9.Y.Dong,C.R.Ramakrishnan,andS.A.Smolka.“ModelCheckingandEvidenceExplo-ration”.InProceedingsofECBS’03,pages214–223,April2003. 10.M.Dwyer,G.Avrunin,andJ.Corbett.“PatternsinPropertySpecificationsforFinite-State Verification”.InProceedingsofICSE’99,May1999. 11.A.GroceandW.Visser.“WhatWentWrong:ExplainingCounterexamples”.InProceedings ofSPINWorkshoponModelCheckingofSoftware,pages121–135,2003. 12.A.GurfinkelandM.Chechik.“Proof-likeCounterexamples”.InProceedingsofTACAS’03, LNCS,April2003. 13.K.Namjoshi.CertifyingModelCheckers.InProceedingsofCAV’01,volume2102ofLNCS. Springer-Verlag,2001. 14.D.Peled,A.Pnueli,andL.Zuck.Fromfalsificationtoverification.InFST&TCS,volume 2245ofLNCS.Springer-Verlag,2001. 15.M.C.PlathandM.D.Ryan.“SFI:AFeatureIntegrationTool”.InR.Berghammerand Y.Lakhnech,editors,ToolSupportforSystemSpecification,DevelopmentandVerification,AdvancesinComputerScience,pages201–216.Springer,1999. 16.L.TanandR.Cleaveland.Evidence-BasedModelChecking.InProceedingsofCAV’02, volume2404ofLNCS,pages455–470.Springer-Verlag,July2002. AToolSupport AprototypeoftheframeworkdescribedinthispaperhasbeenimplementedinatoolcalledKEGVis(Kounter-examplegeneratorandvisualizer).ThetoolisbuiltontopofasymbolicCTLmodel-checkerχChek[3],butanyothersymbolicCTLmodel-checkercanbeusedintheframeworkasablack-boxaswell.Thetoolprovidesseveralviewsoftheevidence,includingahigh-leveloverviewoftheproof,andadetailedproof-likepresentationoftheresultingtraces.KEGVisalsoimplementsalibraryofpre-specifiedexplorationandnavigationstrategiesandenablesuserstocreatetheirown.Abstractioncounterexamplegenerationiscurrentlynotsupportedinourtool. Fig.10.AscreenshotofKEGVis. Figure10givesascreenshotoftwoviewsgeneratedbythetoolfortheButtonmoduledescribedinSection3.3.ThefrontviewshowstheprocessofbuildingaproofofthepropertyEGp,describedinthelastexampleofSection3.3.Forexample,thehighlighteddisjunctionistruebecausethefirstdisjunctholds,whereasthesecondfailstohold.Clickingondifferentpartsoftheproofinthisviewenablestheinteractivebuildingoftheproof. Atanypointoftheproof,userscangeneratethecurrentsnapshotoftheproof-likewitness.ThebackviewinFigure10givesanexampleofawitnessthatcorrespondstotheproofshowninthefrontview.Thewhiteboxesinthisviewrepresentstatesofthemodel,andtheshadedboxescontainsummariesoftheproof.Weshowanenlargementofthestatesofthemodelontheright-handsideoftheview.Notethatsincetheactualmodeloftheelevatordoesnotnamestatesexplicitly,thestatenamesaregeneratedautomatically.Also,theshownconfigurationofthetooldisplaysonlythosevariablesthatchangebetweenstates. 因篇幅问题不能全部显示，请点此查看更多更全内容