αSPIN:Atoolforabstractmodelchecking
Mar´ıadelMarGallardo,Jes´usMart´ınez,PedroMerino,ErnestoPimentel∗
Dpto.deLenguajesyCienciasdelaComputaci´on,UniversityofMalaga29071M´alaga,Spaine-mail:{gallardo,jmcruz,pedro,ernesto}@lcc.uma.es
Publishedonline:9December2003–Springer-Verlag2003
Abstract.Abstractionmethodshavebecomeoneofthemostinterestingtopicsintheautomaticverificationofsoftwaresystemsbecausetheycanreducethestatespacetobeexploredandallowmodelcheckingofmorecom-plexsystems.Nevertheless,thereisalackoftoolsactuallysupportingthistechnique.Onedirectionforabstractingasystemistotransformitsformaldescription(itsmodel)intoasimplerversionspecifiedinthesamelanguage,thusskippingtheconstructionofaspecific(modelchecking)toolfortheabstractmodel.Theabstractionofthemodelshouldbefollowedbytheabstractionofthetemporalfor-mulastobechecked.Thispaperpresentsαspin,atoolfortheintegrationofabstraction(formodelsandformu-las)intothewell-knownmodelcheckerspin.Wepresentthetheoreticalresultssupportingtheimplementationto-getherwithacasestudy.
Keywords:Verification–Modelchecking–Abstraction–spin–Temporallogic
1Introduction
Automaticverificationmethodssuchasmodelcheck-ing[4]havebecomerealistictechniquestobeusedinthedevelopmentofcriticalsystems.However,modelcheckingisonlyeffectivewhenausefulmodelofasystemisavail-able.Byusefulwemeananabstractrepresentationofthesystem,containingonlythedetailsthatensurethatsatis-faction(nonsatisfaction)ofcertainpropertiesprovidesuswithinformationabouttheactualbehaviorofthesystem.Modelsdescribinganexcessofdetailsmayproducethestateexplosionproblem,whichcouldpreventtheuseof
WorksupportedbyprojectsTIC2002-04309-C02-02andTIC2001-2705-C03-02
∗
currenttoolstofullyanalyzethem.Thisproblemaffectsboththesymbolicmethodandexplicitmodelchecking.In[32]itwasrecentlyacknowledgedthatmodelcheck-ingmayprofitfromitscombinationwithabstractinter-pretation[9]toreducethesizeofmodels.However,thistechniqueisnotnew;thefirstpapersformalizingandstudyingthemainproblemsofabstractmodelcheckingwerepresentedbyClarkeetal.[5],Loiseauxetal.[41],Grafetal.[28],andCleavelandetal.[8],tomentionafew.
Applyingabstractmodelcheckinginvolvesdifferentsteps,asenumeratedin[5].First,theoriginalmodel,alsocalledtheconcretemodel,mustbereduced.Toachievethis,weabstractthemeaningofsome“selected”datatypesintheconcretemodel.Thisabstractionmaybedoneusing“abstractionfunctions”[5,10,16],asinthetypicalapplicationsofabstractinterpretation,andalsobymeansofso-called“predicateabstractions”[1,28,43].Second,oncetheabstractmodelhasbeenconstructed,itisnecessarytoredefinethepropertiesinordertoadaptthemtothenewmodelrepresentation.
Theabstractmodelconstructedis,ingeneral,anover-approximationoftheconcreteone;thatis,thenewmodelrepresentsmorebehaviorsduetothelossofinforma-tioninherentintheabstraction.Therefore,animport-antpointtobestudiedinabstractmodelcheckingisthepreservationofthetemporalpropertiesfromtheabstracttotheconcretemodel.Clearly,thereexistsatradeoffbe-tweenobtainingtheleastabstractmodel,producingthesmallestsetofstates,andpreservingasmanyofthemostimportanttemporalpropertiesaspossible.
Theeffectiveapplicationoftheabstractmodelcheck-ingtechniqueinvolvestheconstructionoftoolssupport-ingtheautomaticabstractionofmodelsandproperties.Thispaperpresentsαspin[22],atoolintegratingab-stractmodelcheckingintothewell-knownmodelchecker
166M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking
spin[33,34].Themaincharacteristicsofthetoolaresum-marizedbelow.
αspinrealizesasource-to-sourcetransformationofboththeoriginalmodelandthetemporalproperties.Thisallowsustoreusethesametool(spin)toverifytheab-stractmodel.Toconstructtheabstractmodel,αspinfollowsthe“abstractionfunction”method,substitutingthetypeofcertainmodelvariableswithasimplerab-straction.Usersmayselecttheabstractionfunctiontobeappliedfromanabstractionlibrary,asalsooccursin[14]or[28].Correctnessconditions,studiedin[16],assurethattheabstractmodelgeneratedinthiswaycorrectlysimulates(overapproximates)theoriginalone.
Syntactictransformationmakesuseofxml[45]asin-termediatelanguage[19].xml-associatedtoolsallowustoeasilymanipulatethexmldescriptions.Forinstance,wemayprovethatthenewabstractmodelconstructedcorrectlyfollowsthepromelasyntaxisusingthedtd(documenttypesdefinition)file.
Regardingtheabstractionofproperties,theclassicmethod[5,10]underapproximatestheformulasinthesensethattheirmeaningismorerestrictive.Inotherwords,itismoredifficultforanabstracttracetosat-isfyanunderapproximatedformula.Informally,wemaysaythattheoverapproximationofthemodeliscompen-satedbytheunderapproximationoftheformulas.Con-sequently,thismethodpreservespropertiesfromtheab-stracttotheconcretemodel,thatis,itissuitableforcheckingwhetheratemporalformulaistrueforallexecu-tionpathsintheoriginalmodel.
However,usersmayalsoprefertospecify“bad”non-desirablepropertiesbymeansoftemporalformulasthatnomodeltraceisexpectedtoverify.Infact,spinit-selfprovidesthesetwofunctionalities:theverificationofdesirable(universal)propertiesandtherefutationofnondesirable(existential)properties.Itisworthnotingthatspinimplementson-the-flyautomaton-basedmodelcheckingfollowing[24],whichmeansthatnondesirablepropertiesaredirectlytranslatedintotheautomaton,butuniversalpropertieshavetobenegated(transformedintonondesirableones)beforebeingtranslated.
Whileintheconcreteworldthenegationofadesir-ablepropertygivesusthecorrespondingbadpropertytoberefuted,andviceversa,thistransformationisnotsodirectforabstractproperties.Thereasonforthisisthattheabstractionprocessaffectstheevaluationofnegatedatoms.Therefore,wemaysaythat,ingeneral,theun-derapproximationofa(negated)formulacannotbeuseddirectlytorefuteaproperty.
Oneclearpossibilityfordealingwiththerefutationofabstractpropertiesistryingtoprovethe(universal)satis-fiabilityofthenegationoftheformulatoberefutedusingtheunderapproximatedapproach.Thismethodinvolvesthenegationoftheexistentialformulaanditstransform-ationintothenormalnegationformtoobtaintheinputforspin.Notethatspinwouldtranslateonceagainthenewconstructedformulaintoitsnegation.Adifferentalternativethatavoidsthefirsttrans-formation(notimplementedinspin)consistsindefin-inganewsatisfactionrelationspecificallyorientedtorefutingabstractproperties.In[18,21],weprovedthatthedualapproachtoabstractingpropertiesbasedonoverapproximation,reusingthesametechniquefollowedforabstractingthemodel,canalsobeemployedeffec-tivelyinabstractmodelchecking.Thisapproachnatu-rallypreservestherefutationofexistentialtemporalfor-mulasfromtheabstracttotheconcretemodel.Similaroperatorsfordealingwithnegationintheabstractworldhavealsobeenintroducedin[38–40].Inaddition,in[23]weprovedthatthesemethodsareeffectivelydualinthesensethattheabove-mentionedequivalencebetweenveri-ficationandrefutationisachievedbyusingtheunderandoverinterpretations,respectively.Actually,thesetwoap-proachescanbeconsideredasthetwosidesofthesamecoin,butspecialcareisnecessaryto“turnthecoinover”.Apartfromsavingondevelopmentefforts,usersmaybenefitfromhavingtwowaysofinterpretingabstractfor-mulas.Theycandirectlywritethepropertieswiththe(abstract)interpretationbestsuitedforthegoal.
Furthermore,thesetwopointsofviewhavealsoal-lowedustoobtainmorebenefitsforrefiningtheabstractmodel,asstudiedin[23].Theeliminationof“spurioustraces”(norealistictraces)fromtheabstractmodelisoneofthemajorchallengesinabstractmodelchecking.Thesefalsetracesmayleadtoobtainingfalsenegatives,makingtheabstractanalysisuseless.Solutionsofthisproblemarebasedontheanalysisofcounterexamplestofindoutwhethertheyarerealorfictitious[6,42,43];onmodelre-finementasin[10];orontheapplicationofgeneralresultsabouttheincompletenessprobleminabstractinterpre-tation[25]tothecaseofabstractmodelchecking[26].Ourproposal,however,usesthecombinationofthetwomethodstoconstructformulasthatsimultaneouslyrepre-sentthepropertytobechecked(orrefuted)andthepartofthemodelthathastobeanalyzedtosafelyproveit.Inotherwords,wemakeuseofthemodelcheckingpowertoautomaticallyrefinethemodel.Asaconsequence,thismethodisparticularlyappropriateforon-the-flymodelchecking[7]asimplementedinspin.
Abstractmodelcheckingisalsosupportedbyothertoolsthataremainlyorientedtoprogramminglanguagesandnottoformaldescriptiontechniques.
TheclosesttooltoαspinisBandera[14,30]whichtakesaJavaprogramandproducesaverification-orientedmodelwrittenintheinputlanguageoftoolslikespinorJPF[44].Banderaemploysdependencyanalysistofindfurthervariablestobeabstractedandintegratespower-fulfeatureslikeslicingorautomaticsupporttoconstructsoundabstractionfunctions(withtheassistanceofthetheoremproverPVS).Banderafindsspuriouscounterex-amples,makingsurethatthecounterexamplecontainsnonondeterministicassignments[42].αspinshareswithBanderathedataabstractionmethodbasedontheuseoftheabstractionlibrarytoproduceanoverapproximated
M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking167
model.αspinofferssomefeaturesthatdifferfromBan-dera’s,likeseveralchoicesforconstructingtheabstractmodelforagivenabstractfunction,theuseofunder-oroverapproximationofformulasattheuserlevel,ordeal-ingwiththeproblemofspuriouscounterexamplesbyre-finingtheproperties[23].
OthercloselyrelatedprojectswheredataabstractionisconsideredareFeaVer[37]andabC[12].FeaVerpro-ducesapromelamodelfromannotatedANSICcode.ItemploysalookuptabletomapCinstructionsintopromela.Thismapping,forexample,permitsremovingorreducingtherangeofselectedvariables,producinganeffectsimilartodataabstraction.abCextendsthecom-pilergccwiththeabilitytohidevariablesinsuchawaythatthenewCcodemustincludenondeterministicex-pressionstooverapproximatetheinitialprogram.
Adifferentapproachtoabstractmodelcheckingtoolsistoconstructspecificmodelcheckersthatsupportab-stractionratherthanreusingexistingmodelcheckers.ThisistheideaofJavaPathFinder(JPF)[3,44]andSLAM[2],whicharebasedonthepredicateabstrac-tiontechniqueintroducedin[29].Thistechniqueconsistsinreplacingsomeuser-selectedpredicateswithBooleanvariablesinsuchawaythattheabstractmodelisasafeoverapproximationoftheconcreteone.
JPFisanevolutionofJPF1[31].JPF1usedatransla-tionfromJavatopromela,includingtheabstractioninthetranslationphase.JPFisamodelcheckerthatworksattheJavabytecodelevel.Itsupportspredicateabstrac-tionbyautomaticallytranslatinganannotatedJavapro-gramtoanotherJavaprogram.
ThegoalofSLAMistochecktemporalsafetyprop-ertiesofsequentialCprograms,transformingtheCpro-gramintoaBooleanprogramthatpreservesallcontrol-flowconstructs,butonlyBooleanvariables.
See[11]foramoreextendedsurveyofabstractiontechniquesandassociatedtools.
Thepaperisorganizedasfollows.Section2containssomepreliminarybackgroundonspinanditsinputlan-guages.Sections3and4presentthetheoreticalbasisforsupportingcorrectabstractionbytransformationofpromelaandtemporallogic,respectively.InSect.5,weexplainhowtouseαspinwithapreviouslypublishedliftcontrollersystemasthecasestudy[13].Section6isde-votedtosomeimplementationdetailsofαspin.Inthelastsection,weprovideconclusionsandoutlinesomefuturework.2
PROMELA,LTL,andSPIN
Inthelastfewyears,spinhasbecomeoneofthemostemployedmodelcheckersinbothacademicandindus-trialareas[33,34,36].Itsupportstheverificationofusualsafetyproperties(likedeadlockabsence)insystemswrit-teninthemodellinglanguagepromelaaswellastheanalysisofcomplexrequirementsexpressedwithlinear
temporallogic(ltl).Itisalsousedastheplatformfortryingnewpowerfulalgorithmstoattackthestateexplo-sionproblem.
2.1Modellingwithpromela
promelaisalanguagedesignedfordescribingsystemscomposedofconcurrentasynchronouscommunicatingprocesses.ApromelamodelP=Proc1||...||Procnconsistsofafinitesetofprocesses,globalandlocalchan-nels,andglobalandlocalvariables.Processescommu-nicateviamessagepassingthroughchannels.Communi-cationmaybeasynchronoususingchannelsasboundedbuffersandsynchronoususingchannelswithsizezero.Globalchannelsandvariablesdeterminetheenvironmentinwhichprocessesrun,whilelocalchannelsandvariablesestablishtheinternallocalstateofprocesses.
promelaisanondeterministiclanguagethatbor-rowssomeconceptsandsyntaxelementsfromDijkstra’sguardedcommandlanguage,Hoare’sCSPlanguage,andCprogramminglanguage(Fig.1).Apromelaprocessisdefinedasasequenceofpossiblylabelledsentencesprecededbythedeclarativepart(seeexampleinFig.3).Basicsentencesinpromelaarethosethatproduceadefiniteeffectoverthemodelstate,inotherwords,theassignments,theinstructionsforsending(receiving)mes-sagesto(from)channels,andtheBooleanexpressions,BExp,thatincludetestsovervariablesandcontentsofchannels.Inaddition,promelahasothernonbasicsen-tenceslikethenondeterministicIfandDosentences.2.2Temporallogic
spinverifiesltlformulasagainstpromelamodels.Well-formedformulasoflineartemporallogic(ltl)areinductivelyconstructedfromasetofatomicpropositions(inpromela,propositionsaretestsoverdata,channels,orlabels),thestandardBooleanoperators,andthetem-poraloperators:always“”,eventually“”,next“O”,
Fig.1.Partofpromelasyntax
168M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking
2.3spin
Bydefault,givenanltlformula,spintranslatesitintoanautomatonthatrepresentsanundesirablebehavior(whichisclaimedtobeimpossible).Then,verificationconsistsofanexhaustiveexplorationofthestatespacesearchingforexecutionsthatsatisfytheacceptancecon-ditionsoftheautomaton.Ifsuchanexecutionexists,thenthetoolreportsitasacounterexamplefortheproperty.Ifthemodelisexploredandacounterexampleisnotfound,thenthemodelsatisfiestheltlpropertyasauniversalproperty.Thesameverificationschemecanbeemployedtocheckwhetheraformulacanbesatisfiedbyanypath(refutationofexistentialproperties).Thesetwowaysofusingltlarepresentedinauser-friendlyinterfacecalledxspin,asshowninFig.3.Thefirstcasecorrespondstomarking“AllExecutions”andthesecondoneto“NoExecutions”.
Althoughtherearemanyrealexampleswhereveri-ficationcanbedonewithstandardexhaustiveverifica-tion,spinalsoimplementsoptimizationtechniquestodealwithcomplexsystems.Partialorderreductionre-placesseveralinterleavedsequencesofevents(sentences)withonlyonethatrepresentsthewholeset.Statecom-pressionreducestheuseofmemorybycompressingtherepresentationofthestateswithoutlosinginformation.Bit-statehashingrepresentsstatesasbitsinahashtable,soinmanycasestheanalysisisonlypartial.Ournewtoolpreservestheseoptimizationtechniques.
Intherestofthepaper,whenweusespinwerefertoboththecommand-line-orientedtoolandtoxspin.
Fig.2.LTLsemantics
anduntil“U”.Formulasareinterpretedwithrespecttomodelstatesequencesti=sisi+1....Eachse-quenceexpressesapossiblemodelexecutionfromstatesi.Theuseoftemporaloperatorspermitsconstructionofformulasthatdependonthecurrentandfuturestatesofaconfigurationsequence.ThesemanticsofltlisshowninFig.2,wherepisapropositionandfandgaretemporalformulas.Forthesakeofconvenience,weassumethatallformulasareinnegationnormalform,thatis,negationsonlyappearinpropositions.Notethatwehavenotincludedaruledefiningthesatisfactionofanegatedformula.Instead,wetreattheevaluationofnegatedpropositionsindependentlyoftheircorres-pondingnonnegatedones.ThereasonforthiswillbeexplainedinSect.4.ThelasttworulesinFig.2definethesemanticsoftheuniversalandexistentialtemporalformulas.Notethatsymbols∀and∃arenotltlcon-nectives.Weusethemtosimplifythenotation.There,Mrepresentsthesetofexecutiontracesproducedbythemodel.
Fig.3.Liftsystemmodelandltlformulainxspin
M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking169
3AbstractingPROMELA
Thefirststepforrealizingabstractmodelcheckingistoreducethemodeltobeanalyzed.In[16],wedescribedamethodbasedonthesource-to-sourcetransformationtoabstractpromelamodels.Themainideainthisworkisthatforabstractingmodels,itsufficestoreplacetheoriginalaccessdefinitionsofsomeselecteddataobjectsothattherangeofitspossiblevaluesisshrunkinsuchawaythatthecontrolpartoftheprogram(high-levelop-erationslikenondeterminismselectionandloops,corou-tines,andsoon)remainunchanged.Fromapracticalpointofview,thisobservationisveryimportantbecauseitallowsustoisolatetheprogrampointsthatmustbechangedwhenabstractingamodelindependentlyofthecomplexityofthelanguageconstructions.Inaddition,thismodularvisionfacilitatesthedefinitionofabstrac-tions,theanalysisofthecorrectnessoftheabstraction,andeventheimplementation.
Intherestofthissectionwesummarizethetheoreticalbackgroundsupportingthesource-to-sourcetransform-ationmethod.Inthepresentation,weusethefollowingnotation.GivenasetS,SωdenotesthesetofallinfinitesequencesthatmaybebuiltwiththeelementsofS,and℘(S)isthepowersetofS,thatis,thesetofallitssubsets.LetpromdenotethesetofallpromelasystemsbuiltfollowingthesyntaxgivenbyFig.1.AssumingthatStaterepresentsthesetofallpossiblesystemstates,wedefinefunctions
effect:Basic×State→State
(1)
test:BExp×State→{false,true},
whichdescribetheeffectofexecutingabasicsentenceandatestinagivenstate,respectively.ThesemanticfunctionG(·,effect,test):prom→℘(Stateω)
(2)
associateseachpromelamodelMwiththesubsetofstatesequencesG(M,effect,test)∈℘(Stateω)represent-ingallpossibleexecutiontracesgeneratedbyM,inwhichfunctionseffectandtestareusedwhenexecutingaba-sicsentenceoraBooleanexpression.Notethatfunctionseffectandtestrepresentthestandardimplementationofthemodeldatatypes.
TosimplifytheanalysisofpropertiesoverG(M,effect,test),wemustchooseanadequatesetofre-ducedstates(Stateα,≤α)andastate-to-stateabstrac-tionfunctionβ:State→Stateα
thattransformssetsofconcretestatesintotheirabstrac-tions.Eachabstractdatumisintendedtorepresentasetofconcretestatessharingsomecharacteristicthatisab-stracted.(Stateα,≤α)isusuallyacompletelattice,andthepartialorder≤αrepresentsthedegreeofprecisionofeachabstractstate.
Structure((℘(State),⊆),(Stateα,≤α),α,γ)givesustheGaloisconnectiondefiningtheabstractinterpreta-tionofthemodel,whereα:℘(State)→Stateαandγ:Stateα→℘(State)aredefinedasα(c)=∨State|β(s)≤αsα},respectively.
{s∈c}β(s)andγ(sα)={s∈Finally,toobtaintheabstractbehaviorofthemodelwemustalsodefineabstractversionsofeffectandtest,thatis,functions1
effectαo:Basic×Stateα→State
α
(3)
testαo:BExp×Stateα
→{false,true}
givingthepropermeaningtothebasicpromelasen-tenceswhenexecutedoverabstractstates.Giventhepre-viousdiscussion,
G(M,effectαo,testαo)∈℘((Stateα)ω)
definesanabstractbehavior,moreeasilyanalyzed,forthesamemodelM.
Forinstance,Fig.3showsanexcerptofapromelamodelthatrepresentsthebehaviorofalift(extractedfrom[13]).Tosimplifytheexposition,weassumethatsystemstatesaregivenbythevalueofthevariablePosition[pid],anintegerbetweenthevalues0..(nb_floor−1).Thatis,intheexampleState=[0..(nb_floor−1)].VariablePosition[pid]alwaysstoresthecurrentfloorfortheliftidentifiedbypid.Toreducethemodelsize,considerthelattice(FLOORS,≤α)illustratedinFig.4andtheabstractionfunctionβ:[0..(nb_floor−1)]→FLOORSdefinedas
β(0)=Lower
β(nb_floor−1)=Upper
β(j)=Middle,∀0 1 Subindexodenotesthatabstractfunctionsoverapproximatetheoriginalones.Inthefollowingsections,wewillalsouseindexutodenoteunderapproximation. Fig.4.LatticeFLOORS 170M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking Fig.5.PartoftheabstracteffectforFLOORS leastpreciseabstractdatumsinceitrepresentsanyfloor.Finally,value⊥isusedtorepresentillegalvalues. Theredefinitionofstatesinvolvestheredefinitionoftheeffectofbasicsentences.ThetableinFig.5showsadefinitionof effectαo:Basic×FLOORS→FLOORS (4) fortheinstructions“incrementbyone”and“decrementbyone”,denotedbyinc1anddec1,respectively.3.1Powersetsasabstractdomains Thelossofinformationthatoccurswhenconstructingtheabstractmodelmaybealternativelyrepresentedwithsetsofabstractvalues.Inthiscase,theimprecisionpro-ducedwhenexecutingfunctioneffectαthatoissolvedbygener-atingthesetoftheabstractdatacanbetheresultofthefunction. Forexample,considerthesetAFLOORS={Lower,Middle,Upper} andletPFLOORS=℘(AFLOORS).Function effectαgiveninFig.5mayberedefinedasinFig.6.Notethato thenewfunction effectαo:Basic×AFLOORS→PFLOORS (5) isslightlydifferentfromtheonegivenin(4).Thedif-ferenceliesinthewayeacheffectαproblem.Toexplainthis,ofunctionsolvesthe imprecisionweshouldnotethatideallyfunctioneffectαα(State)=oshouldalwaysreturnoneoftheelementsof{β(s):s∈State},sincethissetcontainsthemostpreciseabstractstates(thelossofin-formationinthesestatesisonlyduetotheapplicationoffunctionβ.)However,whentheresultofeffectαexactlyrepresentedwithoneofthesepreciseocannotbeabstractdata,wemayuseadomainwithimpreciseabstractdata,asFLOORSinFig.5or,alternatively,constructthesetofallpossiblepreciseabstractdatathatcanbetheresultofthefunction,asinFig.6. Fig.6.AbstracteffectforthelatticePFLOORS Thewayofdefiningeffectαasostronglyinfluencestheab-stractmodelconstructed,discussedinthefollowingsection.3.2Correctness Givenanabstractionfunctionβ,itisclearthatfunctions effectαoandtestα omaybearbitrarilydefined.However,theinterestoftheapproachisinpreservingsomecor-rectionpropertiesbetweenthesetsofexecutiontraces G(M,effect,test)andG(M,effectαα In[16,18],thereisanexhaustiveo,teststudyo). ofthecor-rectnessconditionsthattestαbeacorrectoandeffectα overapproximationomustverifyfor G(M,effectαo,testα o)toofG(M,effect,test). Insummary,theseconditionsmaybewrittenasfol-lows.Givenp∈Basicandb∈BExpandtwostatess∈State,sα∈Stateαsuchthatβ(s)≤αsα,then β(effect(p,s))≤αeffectαo(p,sα ), (6) test(b,s)⇒testαo(b,sα ). (7) WhenusingPowerSets,theconditionsetby(6)isre-placedbythefollowingone: β(effect(p,s))∈effectαo(p,sα ). (8) Correctnessconditionsguaranteethattheabstractmodelsimulatestheoriginaloneinthesensethatforeachnondeadlockedtrace t=s0s1···∈G(M,effect,test)thereexistsanondeadlockedabstracttrace tα=sα0sα1···∈G(M,effectαo,testα o) thatoverapproximatesit.Wedenotethisrelationbyβ(t)≤αtα,whereβ(t)=β(s0)β(s1)...,anddefineitas β(t)≤αtα⇔∀i≥0.β(si)≤αsαi.Forinstance,theconcretetracet=0inc1 1inc1 2dec1 1dec1 0skip ... couldbeapproximatedbytheabstracttracetα=Lowerinc1 Middleinc1 noLower dec1 noUpperdec1noUpperskip .... (9) Wehavelabelledeachtransitionwiththebasicin-structionexecuted,andwehaveusedthetableinFig.5torealizeeachabstracttransition. Notethatweexplicitlyexcludedeadlockedtracesbe-causetheabstractionprocessmaymodifythissafetypropertyofthesystem. M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking171 Inthepreviousexample(9),weimplementedthelossofinformationwhenexecutingabstractoperationsusingspe-cificabstractconstants.However,asdiscussedinSect.3.1,wecouldhaveusedsetsofabstractdatainstead.Forex-ample,whenthevalueMiddleisincremented,wecouldusetheset{Lower,Middle}insteadofnoUpper. Fromtheimplementationpointofview,theuseofsetsimpliesutilizingnondeterministicassignmentswhenupdatingabstractedvariables,whichprovokesthedirectcreationofseveralbranches.Followingtheexample,thismeansthattheabstractionoftproducesmorethanoneabstracttrace.InFig.7,weshowtheabstracttracesin G(M,effectαα haveusedo,testthedefinitiono)overapproximatingt,assumingthatweofeffectαandFig.6. ogivenbytheexpres-sion(5)Incontrast,theuseofabstractdomainsdefinedadhoc,like(9),eliminatestheuseofnondeterministicas-signmentsandallowsustodelaythecreationofbranchesuntilatestoftheupdatedvariableisfound.Thismeansthat,inmanycases,thismethodproducessmallerab-stractmodels,i.e.,itrealizesamoreeffectivereductionoftheoriginalmodel.Forexample,regardingFig.7,theabstractmodelwiththespecificabstractconstantsof(9)issmallerthanwithnondeterministicassignments.Incontrast,sincetheabstracttracesaremoreimpre-cise,possiblysomeinformationrelevantforprovingcer-taintemporalpropertiesmayhavebeenlost.However,inothercases,theuseofmorevaluesintheabstractdomain(sevenforFLOORS)thaninthepower-set-basedmethod(threeforPFLOORSorfouriftheIllegalvalueisalsoconsidered)producesworseresultsforthefirstmethod.Ingeneral,thesizeofthestatespaceforeachmethoddependsonhowthemodelproducesthevalues,andwecannotsaythatoneisalwaysbetterthantheother. Asbothimplementationapproachesproducecorrectoverapproximationsofthemodel,wehaveincludedthetwomethodsasoptionsinαspin,allowingtheusertoexperimentforbothagivenmodelanddifferentopti-mizationoptions.Itisworthnotingthatpreventingnewnondeterministicsentencesintheabstractmodelpermitsusingthe“statementmerging”optimizationdescribedin[35].Thismaybeaveryinterestingpointinfavorofusingtheabstractconstantsmethodforsomesystems.Whenappliedtofunctiontest,thenotionofover-approximation,givenby(7),meansthatfunctiontestαalwaysproducesasaferesult,thatis,itmustreturntrueoiffinsomeconcreteexecutionthevaluetruemaybere- Fig.7.AbstractionoftusingPowerSets turned.Thus,givenp∈BExp,andsα∈Stateα,functiontestαoisdefinedas testαo(p,sα )= test(p,s)(Over). {s∈State.β(s)≤αsα} Inaddition,inthefollowingsection,wewillalsomakeuseofthistestαmationmethodofunctiontoimplementtheoverapproxi-forevaluatingtemporalformulas.3.3Syntactictransformationofpromela ThesyntactictransformationofapromelamodelMtoobtainanewmodelMαisbasedonreplacingeachba-sicinstructioninMbyastandardpromelacodethat implementstestαoandeffectα o.Thentheverificationiscarriedoutbyonlyexecutingstandardpromelainstruc-tions.Thisapproachcorrespondstoimplementingaveri-fierforG(Mα,effect,test). Forinstance,thenextcodeshowsFLR_INC,apos-sibleimplementationofabstractincrementinc1definedinFig.5. #defineFLR_INCR(x)if ::x==Lower->x=Middle\\::x==Middle->x=noLower\\::x==noUpper->x=noLower\\::x==noLower->x=noLower\\::x==Unknown->x=noLower\\::else->x=ILLEGAL\\ fi Followingtheideasdiscussedintheprevioussections,itisalsopossibletoimplementadifferenteffectαFig.6asfollows. ofunc-tion,usingthetablein#defineFLR_INCR(x)if ::x==Lower->x=Middle\\::x==Middle->x=Middle\\::x==Middle->x=Upper\\::else->x=ILLEGAL\\ fi Inthesetwocodes,theconstantILLEGALisemployedtorepresent⊥. ThecodeinFig.3isnowreplacedbythenextone,whichillustratestheuseoftheabstractinstruction(effectαo)toincreasethevariablePosition[]. proctypeLift(intpid){intOrder=null;do... ::SysLift_Lift[pid]?Order; if ::(Order==Up)->FLR_INCR(Position[pid]);...} Notethattheabstractcodeconstructedisindepen-dentoftheimplementationofFLR_INCR. Thesamemethodisemployedtoimplementtestαo.Forexample,thenextdefinitioncontainstheimplementationofFLR_EQ(abstracttestfor(i==j)) #defineFLR_EQunder(x,y) ((x==Lower&&y==Lower)||(x==Upper&&y==Upper)) 172M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking #defineFLR_EQimp(x,y)( ((x==Upper)&&(y==noLower))||((x==noLower)&&(y==Upper))||((x==Lower)&&(y==noUpper))||((x==noUpper)&&(y==Lower))||((x==Middle)&&(y==noUpper))||((x==noUpper)&&(y==Middle))||((x==Middle)&&(y==noLower))||((x==noLower)&&(y==Middle))||((x==Middle)&&(y==Middle))||((x==Unknown))||((y==Unknown))) #defineFLR_EQ(x,y)(FLR_EQimp(x,y)||FLR_EQunder(x,y)) FunctionFLR_EQverifiesthecorrectnessconditions (studiedin[16])necessaryfortheabstractmodeltocor-rectlysimulatetheoriginalone.Informally,FLR_EQ(x,y)istruewhena==bholdsforsomeconcretedataaandbab-stractedbyxandy,respectively,asdefinedin(Over)equa-tion.ThisexplainswhyFLR_EQ(Upper,noLower)returnstrue.ThereasonfordefiningFLR_EQusingtwomacros(FLR_EQunderandFLR_EQimp)willbeexplainedbelow.Animportantpointisthattheuseronlyhastoselectsomevariablestobeabstractedandtheabstractiontobeapplied(β).Thenαspinautomaticallyabstractsthesevariablesaswellasanyothervariablerelatedtotheonesselected.Theselectionisdonethroughagraphicaluserinterface,wheretheusercaneasilyseetwokeydata:thevariablesinthemodel(presentedinahierarchicway)andthefunctionsavailableintheabstractionlibrary.Anex-amplewillbeshowninthecasestudysection(Fig.14). 4Abstractingtemporallogic Oncethemodelhasbeenreducedusingthemethodde-scribedintheprevioussection,thefollowingstepistodefinethesatisfactionofatemporalformulaovertheab-stractmodel(whichiscalledtheabstractsatisfaction)andtorelateitwiththesatisfactionoftheformulaovertheoriginalone. Atomicpropositionsinltlformulas,whencheckingpromelamodels,areBooleanexpressions.Thus,consid-eringthestandardnotionofsatisfiabilitygiveninFig.2,andfollowingthesameideausedforabstractingthemodel,wemayassertthat,todefinetheabstractsat-isfactionofatemporalformula,itsufficestodefinetheabstractsatisfactionoftheatomicpropositions. Oneclearpossibilityistousethefunctiontestαdefinedintheprevioussection(Over),toevaluateo,astheatomicpropositions.Usingtestαoverapproximationmethodoleadsustoconstructtheso-calledforabstractingtem-poralformulas,whichhasbeenstudiedatlengthin[18].Analternativepossibilityistousethefollowingfunc-tiontestαutoevaluatetheatomicpropositions.Givenp∈BExpandsα∈Stateα,testαuisdefinedas testαu (p,sα )= test(p,s)(Under).{s∈State.β(s)≤αsα} Classicpapersintegratingmodelcheckingandab-straction[5,10]usefunctiontestαutoevaluatetemporal formulas.Functiontestα oincorporatesthedualmethodthatmaybeofinterestinsomeoccasions,asdiscussedinthenextsection.4.1Preservationresults Inwhatfollows,wesummarizethemaintheoreticalre-sultsconcerningthetwomethodsofabstractingprop-ertiesandalsodiscusstherelationbetweentheab-stractsatisfactionoftemporalformulasovertheab-stractmodel(usingboththeclassicandtheoverapprox-imatedmethod)andthesatisfactionovertheconcretemodel. Intherestofthissection,wewrite:1.s|=pifftest(p,s)holds, 2.sα|=α3.sα|=opifftestααo(p,sα )holds,and upifftestαu(p,sα )holds.Wealsoextend|=,|=αo,and|=αutoabstracttracesdefiningthemeaningoftemporaloperatorsasinFig.2.Notethat,forinstance,whenwewriteMα|=αmeanthat∀tα∈G(M,effectαααα u∀f,we isworthrecallingo,testthato),t|=wealwaysuf,andsoon.Finally,itassumethattemporalformulasareinnegationnormalform,evenwhenweuseformulaslike¬f. Inthiscontext,theinterpretationoftestαpropositionoisthatan abstractstatesα satisfiesanatomicp,iffsomeofitsconcretizationssatisfyp.Thatis,followingthepreviousnotationandassumingthatβ(s)≤αsα,wemaywritethisass|=p⇒sα|=αop. (10) Inaddition,extendingthisresulttoabstracttracesand temporalformulas,weobtainthepreservationofprop-ertiesfromconcretetracestoabstractones.Thus,givenatemporalformulafandtwotracest,tαsuchthatβ(t)≤αtα,wehavethatt|=f⇒tα|=αof. (11) Dually,functiontestαuassertsthatanabstractstatesαsatisfiesagivenatomicpropositionpiffallitsconcretiza-tionssatisfyp.Thus,assumingthatβ(s)≤αsαandβ(t)≤αtα,weobtainthetwofollowingresultsregardingfunctiontestαu: sα|=αup⇒s|=p(12) tα|=αuf⇒t| =f,(13) whichmeansthattestαuallowsustopreservetemporalpropertiesfromtheabstracttotheconcretetraces. Thefollowingtheorempresentstwodirectresultsofthepreviousdiscussion.Inthetheorem,weassumethat G(M,effectαo,testα o)isacorrectoverapproximationofmodelG(M,effect,test)inthesensedescribedinthepre-vioussectionandthattheoriginalmodelisdeadlockfree. M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking173 Theorem1.GivenatemporalformulafMα|=αu∀f⇒M|=∀f(14) Mα|=αo∃f⇒M| =∃f.(15) Thefirstresult((14)),whichiseasilyprovedusing (13),correspondstotheclassicweakpreservationofuniversalpropertiesstudiedin[10].Usingtheclassicmethodology,thesatisfactionofuniversalpropertiesisdi-rectlypreservedfromtheabstracttotheconcretemodel.Thesecondresult,whichcanbeeasilyderivedfrom(11),isthedualpreservationresult.Usingthedualmethod,therefutationofexistentialpropertiesisdirectlypre-servedfromtheabstracttotheconcretemodel.Notethattheremaybecaseswheretheabstractmodelfailstore-vealanyinformationaboutagivenpropertybecauseitfailstodemonstrateeither(14)or(15).4.2Dealingwithnegation Notethatresults(14)and(15)arenotequivalentbecausebothmethodsdealwithnegationusingnonstandardanddualapproaches.Webrieflydiscussthisbelow. Considerapropositionp,anabstractstatesαα∈State,andtwostatess1,s2∈State,verifyingβ(s1)≤αsα,β(s2)≤αsα,thatis,twoconcretizationsofsα.•Assumethats1|=pands2|=¬p.Then,bydefinition(Under),(orequivalentlyusing(12)),wehavethat sα|=αup,sα |=αu¬p (16) whichmeansthatusingtheclassicmethod,itispos-siblethatanabstractstatedoesnotsatisfyaproposi-tionoritsnegation. •Assumenowthats1|=pands2|=¬p.Then,bydefin-ition(Over),(orequivalentlyusing(10)),wehavethat sα|=αop,sα |=αo¬p. (17) Therefore,withtheoverapproximationmethod,itispossiblethatanabstractstatedoessatisfyaproposi-tionanditsnegation. Extending(16)and(17)totracesandmodelswemayassertthat Mα|=αu∃f⇒Mα|=αu∀¬f (18) Mα|=αo∀f⇒Mα|=αo∃¬f (19) whichmeansthat,ingeneral,wecannotusetheclassicmethodforrefutingpropertiesand,atthesametime,wecannotusetheoverapproximationmethodtoverifyuni-versalproperties. However,itcanbeproved[23]that,givenanabstractstatesα∈Stateαandanatomicpropositionp∈BExp,thefollowingequivalenceholds: testαu(p,sα)⇔!testαo(¬p,sα ) (20) or,usingtheequivalentnotation, sα|=αup⇔sα |=αo¬p. (21) In(20),weusethesymbol“!”toindicatethestandard negation.Finally,extendingthisresulttomodels,weob-tainthefollowingtheorem: Theorem2.Givenatemporalformulaf Mα|=αu∀f⇔Mα |=αo∃¬f. Thetheoremassertsthattheclassicmethodmayprovethesatisfactionofapropertyovertheabstractmodelifftheoverapproximationmethodmayrefuteitsnegation.Inotherwords,theresultsaysbothmethodsareequiva-lentlyaffectedbytheabstractmodel.Inaddition,ascom-mentedintheintroduction,thisequivalencealsomeansthatwemayimplementeithermethodusingtheotherone.Consideringthatweimplementedtestαmorereasonableoforabstractingthemodel,itseemstobetodefinetheclas-sicmethodasafunctionoftheoverapproximatedone.Inanycase,fromtheuser’spointofviewitisveryinterestingtoemploytheabstractmodelcheckerαspinfollowingthespinphilosophy:satisfactionandrefutation. Thetwofollowingsectionsaredevotedtoexplaininghowαspinimplementstheabstractionofformulas.Sec-tion4.5showsthemainapplicationoftheintegrationoftheclassicandoverapproximationmethods:theauto-maticrefinementofabstractmodels.4.3SyntactictransformationofLTL Thesyntactictransformationoftemporalformulas(forbothapproaches)isstraightforwardonthebasisofthepreviousdiscussion.Thefirststepconsistsofwritingtheformulainnegativenormalform(ifnecessary).Thenthepropositionsareautomaticallyreplacedbytheabstractimplementationofthetest,dependingonthemethodtobeemployed.Fortheimplementationoftheover-approximationmethod,propositionsaredefinedusingthesamedefinitionoftestαoemployedtotransformthemodel.Similarly,weimplementtestαthecriterionu,whichismorerestrictive thantestα o,toensuredefinedabove(Under). Thus,ifpisanatomicpropositionandpαα denotetheevaluationofpdefinedbytestαuandpα o spectively,wehavethat oandtestu,re-sα|=αop⇔sα |=pαo (22) sα|=αup⇔sα |=pαu. (23) Byinductivelyextending(22)and(23),andusingfα andfuα todenotetheimplementationoftheabstractsat-oisfactionoffusingtheoverapproximationmethodandtheclassiconeasbefore,weobtainthefollowingequiva-lencesregardingtemporalformulas:tα|=αof⇔tα| =foα (24) tα|=αuf⇔tα| =fuα ,(25) 174M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking whichmeansthatwemayusetheusualsatisfiabilityre-lation|=(theoneimplementedbyspin)toevaluatetem-poralformulasusingboththeoverapproximationmethodandtheclassicone.Therefore,oncewehaveimplementedthetwodifferentmethodsofabstractingtemporalformu-las,allresultspreviouslydiscussedmaybeappliedusingspin. Inparticular,theassertionsprovedbyTheorems1and2mayberewrittenasfollows: Mα|=∀fuα ⇒M|=∀f (26) Mα|=∃foα ⇒M|=∃f (27)Mα|=∀fuα ⇔Mα|=∃(¬f)αo. (28) Forinstance,adefinitionlike #defineFLR_EQunder(x,y)((x==Lower&&y==Lower)|| (x==Upper&&y==Upper)) implementsthe(classic)abstracttestfor(i==j).Infor-mally,FLR_EQunder(x,y)istruewhena==bholdsforallconcretedataaandbabstractedbyxandy,re-spectively,asdefinedin(Under).NotethatFLR_EQ(de-finedinSect.3.3)usesthetwomacrosFLR_EQunderandFLR_EQimptoconsiderthecaseswhereonlysomecon-cretestatessatisfy(i==j).InSect.5,wepresentseveralexamplesofformulatransformation.4.4On-the-flymodelcheckingandabstraction Ascommentedintheintroduction,spinimplementson-the-flymodelchecking[7].ThismeansthatgivenamodelMandatemporalformulaf,toproveM|=∀fthetoolproceedsasfollows:themodelMisconvertedintoacor-respondingB¨uchiautomatonAM,thenegationoff,!f,isalsotranslatedintoanotherautomatonA!f,andthentheemptinessoftheintersectionofAMandA!fischecked.Whentheformulafrepresentsapropertytoberefuted,thatis,wewanttocheckM|=∃finstead,theapproachissimilar,exceptthatfisnotnegatedbeforebeingtrans-latedintotheautomaton. Whenappliedtoabstractmodelchecking,theon-the-flymethodworksinasimilarfashion.Thatis,tocheck Mα|=∀fuα ,thetoolconstructsanautomatonAMαrep-resentingtheabstractmodel,anotherautomatonA!fαrepresentingthenegationoftheformulatobeproved,uandtriestochecktheemptinessoftheintersectionof AMαandA!fα.However,u itisinterestingtonotethattheextensionof(20)toabstracttracesmayalsobewrittenusingthenotationintroducedintheprevioussectionas tα|=fuα ⇔tα|=(¬f)αo (29) orequivalentlyas tα|=!fuα ⇔tα|=(¬f)αo, (30) whichmeansthattheabstractformula!fαto(¬f)α uisequivalent o. Continuingwiththepreviousdiscussion,thismeans thatcheckingtheemptinessofAMαandA!fαislikecheckingtheemptinessofAu MαandA(¬f)α.Thatis,thetoolconstructsequivalentautomatatoproveo Mααspinalways|=αandMα|=α worksu∀f withoverapproximatedo∃¬f.Inotherwords,versionsofboththemodelandtheproperty. Forinstance,assumethatauserwantstoprovethesatisfiabilityofauniversalpropertyfonanabstractmodelMα.He/shemaydirectlyconstructthepropertyfuαandgivesittospin.Thenspinconstructstheautoma-toncorrespondingto!fuαthatisequalto(¬f)αspinhasautomaticallyconstructedo,whichmeansthattheover-approximatedversionof¬f. Inthiscontext,itisinterestingtonotethatimple-mentingrefutationwithoverapproximationischeaperthanusingunderapproximation,althoughfromatheoret-icalpointofviewtheyareequivalent(see(28)).Thisfactisshowninthenextexample. ∃(pos==0) neg+nnf+under over ∀(¬(pos==0))αu ∃(pos==0)αo neg+nnf(xspin) ∃!(¬(pos==0))αu trans(xspin) trans(xspin) Automaton Usingonlytheunderapproximationapproach,tore-futetheformula(pos==0),wehavetoproceedas shownintheleftbranch.Thefirststepistonegatetheformula,obtainitsnegationnormalform(nnf),andun-derapproximatethenegatedpropositions.Thisnewfor-mulaisthengiventospin/xspintobecheckedasauni-versalformula,thatis,xspinnegatesitagainbeforetranslatingitintotheautomaton.Incontrast,usingtheoverapproximationapproach,theonlyworktobedoneoutsidestandardxspinistheformulaoverapproximation(shownintherightbranch).Bothcasesproduceequiva-lentautomata.4.5RefinementofLTL Themainprobleminabstractmodelcheckingoccurswhentheanalysisofagiventemporalpropertyisnon-conclusiveduetotheincompleteness/imprecisionoftheabstractmodel. Theorem1provedthatMα|=α=∀fever,ingeneral,iftheanalysisofMuα∀f|=⇒α M| .How-ifMα|=αu∀fu∀f,wecannotconcludethatM| =fails,∀f.thatThisis,isbecausetheabstractmodelMα mayincludeaso-called“spurioustrace”,thatis,anabstracttracethatabstractsnoconcreteoneanddoesnotsatisfyf.Atthesametime,thefactMα|=αo∃fdoesnotmeanthatM|=∃f,forthesamereasons. M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking175 Ascommentedintheintroduction,theeliminationof“spurioustraces”fromabstractmodelshasbeentradi-tionallysolvedbymeansoftheprocessofmodelrefine-ment,asin[6],[26],or[42].In[23],weproposedanal-ternativeapproachforimprovingtheprecisionofabstractmodels,especiallysuitableforon-the-flyabstractmodelchecking.Theideaistoconstructatemporalformulaex-pressingboththepropertytobechecked(orrefuted)andalsothepartofthemodelthatmustbeinspectedinsuchawaythatwhilethetoolischeckingtheformula,themodelisbeingautomaticallyrefined. Toconstructthese“refinerformulas”,wehavetoin-tegratethetwomethodsexplainedaboveforabstractingtemporalformulasasfollows.Giventwotemporalformu-lasfandg, M|=∀gandMα|=∀(gαo→fuα )⇒M|=∀f (31)M|=∃gandMα|=∀(foα→gα u)⇒M|=∃f. (32) Theresulting(31)maybeusedtoprovedesirableproperties,while(32)isthedualresultforrefutingnon-desirableproperties.Inbothexpressions,gisthepartoftheformulathatrefines,andfisthepropertytobeproved(refuted). Forinstance,(31)maybereadasfollows:ifitisknownthatmodelMsatisfiestheuniversalpropertyg,inordertochecktheuniversalformulaf,thetoolshouldonlyin-spectthatpartoftheabstractmodelthatsatisfiesgα satisfygo.All abstracttracesthatdonotα readsimilarly.Notethattheoare“spurious”.(32)maybetechniquepresentedhereisuselessforfindingerrorsintheoriginalmodel.Itsutilityisonlytoeliminateabstractspurioustracestoimprovetheverificationorrefutationoftemporalprop-erties.Itisclearthatwehavetoensurethattherefinerformulaholdsbeforehand,verifyingit,forexample,ontheabstractorontheconcretemodel(ifpossible). Oneapplicationoftheseresultsistheeliminationoftheabstractspurioustracescontainingnonprogresscy-clesinabstractmodels.Abstractionmethodsnormallyintroducethesetraces.Forinstance,itisusualthattheabstractionprocesstransformsterminatingloopsintonondeterministicloops,includingnonprogresscycles.Manylivenesspropertiesmaybeviolatedbyabstracttracescontainingthesecycles. TheanalysisofMα|=∀(gαo→fuα )mayberealizedusingonlytheoverapproximatedversionsofthetemporalformulas,withtheequivalentexpression Mα|=∃(gα o∧(¬f)αo) asimplementedinαspin.5Usingαspin:acasestudy Inthissection,wedescribethemainfunctionalitythat αspinaddstospin/xspin.Ourcasestudyisavariantofthepromelacodeforanelevatorcontrollerpresented in[13].Weshowhowtoemploythedualapproaches fortherefutationandverificationoftemporalproper-ties.Thefirstexperimentistodiscarderrorsbyrefuta-tion(withtheoverapproximationmethod).Thesecondoneconsistsincheckingadesireduniversalpropertywiththeclassicmethod.Thenweshowhowtousearefinerformula.5.1Themodel Theoriginalspecificationin[13]considersacontrollersystemtomanagenlifts,andouraimistoverifythatthesamecontrolstructurealsoworksforonlyonelift.Fol-lowingtherulesabouthowtoconstructsuitablemodelsforverification(see[34]),wehavemadeasetofchangestoworkwithonelift(seeschemeinFig.9).TheliftisrepresentedwiththeLift()processthatreceivesorderstomoveUpandDownandtoStop,thusupdatingitsPosition.ThecontrolpartreceivestheinputsandsendstheorderstotheLift()process.Thispartisdividedintoseveralprocesses–(SysLift(),SysStop(),andSysPanel())–thatcommunicateviarendezvouschan-nelsandglobalvariables.TheschedulingofthewholesystemismanagedbytheprocessSampler()usingren-dezvouscommunication.ThemainvariabletocontroltheflowineveryprocessistheglobalvariablePosition,whichalwaysstoresthecurrentfloorforthelift. Theinputstothesystemareuserrequestsfromin-sidethelift(internalrequests).Thependingrequeststomovetospecificfloorsarestoredbytheglobalarrayinternal_request[nb_floor],nb_floorbeingtheac-tualnumberoffloorsinthesystem.ThecodeinFig.3showstheupdatingofthisvariableintheLift()processdependingontheorderfromthecontrolpart(Up,Down,Stop). Theenvironmenttoverifythissystem,thatis,thevariablepart,shouldbedefinedinsuchawaythatallpos-sible(legal)inputscanbeproduced.Inourmodel,thisenvironmentconsistsoftwopiecesofcode,oneinprocessSampler()andtheotheroneinprocessinit(),asshowninFig.8. ThecodeinSampler()simulatestheinternalre-quests,whereasthecodeininit()isusedtodecidetheinitialpositionofthelift(inanondeterministicway).Figures11to13showatypicalbehaviorofthewholesystem(asimulation).Notethatspincarriesoutastep-by-stepexecution,allowingtheinspectionofcodeandvariablesineverystep. ThesizeofthestatespaceproducedbythismodelisshowninTable1(rowsafetyinconcretemodel).Notethatthestatespaceincreasesexponentiallywiththenumberoffloorsinthelift.5.2Discardingerrors Onecriticalpropertyforcheckingwhetherthecontrolsystemworksproperlyistheabsenceofmovementinthe 176M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking Fig.10.Typicalscenariointheconcretemodel NoMove:<> <> Fig.8.Partoftheconcretemodel (configured&& ((posL&&[]no_request&&<>posU)||(posU&&[]no_request&&<>posL))) absenceofrequests.ThepropertyNoMovesaysthat“theliftnevergoesfromoneextremetotheotherwith-outanyrequest”.Thispropertycanbeencodedasthetemporalformula andthenwecanuseαspintoverifythattherearenoexecutionssatisfyingtheformula.PropositionsposLandposUindicatewhethertheliftiscurrentlyatthelowerorupperfloor,respectively.Propositionno_requestrepre-sentsthattherearenorequestsforthelift.Thesepropo- Fig.9.Liftsystemscheme M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking177 Fig.11.Simulationsteps Fig.13.Variablesintheconcretemodel Fig.12.Theconcretemodel sitionsaredefinedaccordingtotheirinterpretationstan-dardorabstractasdefinedinSect.4.Thenextdefinitionscorrespondtothestandardinterpretation(consideringfourfloors): #define#define#define#define configuredposUposL no_request (config==true) (Position[0]==(nb_floor-1))(Position[0]==0) ((internal_request[0]!=true)&&(internal_request[1]!=true)&&(internal_request[2]!=true)&&(internal_request[3]!=true)) Thepropositionconfiguredisincludedtoensurethatthepropertyischeckedonlywhenthewholesystemhasbeeninitialized. Themainprobleminverifyingtheconcretemodel(withstandardmeaningforpropositions)isthatthe verificationtimeishighlydependentonthenumberoffloors,anditisnotscalablewhenthisparameterisin-creasedtohighvalues.Fortunately,propositionsintheformulaNoMovegiveusaguideonhowtoabstract.AstheevaluationofthesepropositionsmainlyreliesonthevalueofthevariablePosition[0],andthisvariableisusedasacounter,wecouldemploytheFLOORSab-stractiontoreducethestatespacetobevisited.How-ever,theuseofFLOORSimpliesthattheglobalarrayinternal_request[nb_floor]hastobeabstractedbyanarraywithonlythreecomponents.Thisworkisdonebytheabstractiontoolbyanalyzingthestructureofthemodel,usingtheuserselection. TheGUIinFig.14providesinformationaboutthevariablescontainedwithinthemodel(name,type,andcontext:globalorlocal),aboutthetemplatesavailableintheabstractionlibrarysuitableforthevariablesinthe Table1.Verificationresults Floors ConcreteModel SafetyMoveNoMoveSafetyMoveNoMove 3456789 9826941.12038e+061.9656e+06 345534787050 10 2.4392e+062.76741e+064.87864e+06 352235467184 27727942215825746715069238844031849164249746643617356644517956201598343286115079301552777071305330706246 312031386380 318732066514 325432746648 332133426782 338834106916 AbstractModel 178M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking &&ARRAY_ISNOTSET(internal_request, FLR_Map(FLR_LOW,FLR_HIGH,(nb_floor/2)),true) &&ARRAY_ISNOTSET(internal_request, FLR_Map(FLR_LOW,FLR_HIGH,(nb_floor-1)),true)). temporalformula,thecurrentbindingofvariablestoab-stractionfunctions,andasuggestiontoabstractsomevariables(Position[]).Thissuggestionisinitiallymadeforthevariablesinvolvedinthetemporalformula,anditisfurtherextendedtoothermodelvariablesdirectlyre-latedtothefirstset.Forexample,thelocalvariablefintheprocessSysPanel()shouldalsobeabstracted.Whentheabstractionfunctionshavebeenselected,αspinau-tomaticallyperformsboththesyntactictransformationofthepropertyandthemodel,dependingontheuser’schoice. 5.2.1Transformingtheproperty Whenthechoiceiserrorbehavior(PropertyholdsforNoExecutions),asshowninFig.15,theformulaistrans-formedusingtheoverapproximationmethod,thatis,thepropositionsareredefinedasfollows: #defineconfigured(config==true)#defineposUFLR_EQ(Position[0], FLR_Map(FLR_LOW,FLR_HIGH,(nb_floor-1))) #defineposLFLR_EQ(Position[0], FLR_Map(FLR_LOW,FLR_HIGH,0)) #defineno_request (ARRAY_ISNOTSET(internal_request, FLR_Map(FLR_LOW,FLR_HIGH,0),true) NotethatFLR_EQ,whichwasalreadyusedasanex-ampleinSect.3.3,isdefinedwithtwoparts,thepre-cisepart(FLR_EQunder)andtheonethataddsimpre-cision(FLR_EQimp).ARRAY_ISNOTSETchecksthatanar-rayelementgivenbyindexdoesnotcontainvalue.BothmacrosFLR_EQ,andARRAY_ISNOTSETimplementtheoverapproximatedtestαfunction.Theirdefinitionsaregeneratedautomaticallybyαspin. ThemacroFLR_Mapimplementsthefunctionαas #defineFLR_Map(min,max,item)((item>=max)->Upper: ((item<=min)->Lower: Middle)), anditisusedwhenitisnecessarytoobtaintheabstractvalueforagivenitem.5.2.2Transformingthemodel The(simultaneous)transformationofthemodelem-ploystheimplementationofthe(overapproximated)ab-stracttestandeffectforFLOORS.Inaddition,bydefault,αspinproducesthemoreabstractmodel,whichuses Fig.14.Oneviewinαspin M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking179 Normalizationisparticularlyimportantwhendealingwithelse.Forinstance,considerthefollowingcodeup-datingthevariablevtherangeofwhichis[0..10]. if ::v==2->v++::else->v--fi IfweabstractthiscodewithFLR(FLOORS)as if ::FLR_EQ(v,Middle)->FLR_INC(v)::else->FLR_DEC(v)fi thentheabstractmodeldoesnotcorrectlyapproximatetheconcreteone.Forinstance,whenv==3,theconcretemodelonlyexecutesthesecondbranch,whiletheab-stractcodeaboveonlyexecutesthefirstone(probablyleadingtoaspurioustrace).Thenextnormalizedcodecorrectlyoverapproximatesthemeaningofelse(v!=2). if ::FLR_EQ(v,Middle)->FLR_INC(v)::FLR_NE(v,Middle)->FLR_DEC(v)fi Fig.15.Refutationoferroneousbehaviors theabstractvaluesUnknown,noLower,andnoUpperinthemodel.ThecodeinSect.3.3showspartofthefi-nalcodeforprocessLift().Asanadditionalexample,Fig.16andFig.17show,respectively,theconcreteandtheabstractversionsoftheprocessSysStop().Notethattheabstractversionhasbeenautomaticallynor-malized,replacingtheguardelsewithitsabstractmeaning. Nowthetwobrancheswillbeexecutedwhenv==3.NotethatweomittedtheuseofFLR_Mapforreadabilityreasons. αspinconsidersothernormalizationruleswhenap-plyingabstraction.Forexample,itreplacesexpressionslikei=i+1andi=i-1with,respectively,i++andi--.Inthiscase,theabstracteffectofincrementanddecre-mentismoreprecisethanthedirectabstractversionsoftheinitialsentences. Fig.16.ConcreteversionofSysStop 180M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking Fig.17.AbstractversionofSysStop Linkstothewholeabstractmodel,includingthedefinitionoftheabstracttestsandeffects,aregivenintheappendix. 5.2.3Checkingtheproperty AsshowninFig.15,withthistransformationtheerrorNoMoveisnotpresentineithertheabstractmodelor,usingTheorem1,theconcretemodel.Thebenefitsofusingtheabstractformulatodiscardthiserroraresum-marizedinTable1andFig.19.Theexpectednumberofvisitedstatesisgreatlyreducedcomparedtotheconcretemodel.Furthermore,thevariationofthenumberofstatesislinearwithrespecttothenumberoffloors.5.3Verificationofadesiredbehavior Afterdiscardingthekeycriticalerrorbehaviors,wepro-ceedbyverifyingthattheliftsystemworkstoprovidetheintendedservice.Forexample,thepropertyMovesaysthat“incaseofrequestfromthelowerfloor,theliftalwaysstartsthemovementtolower”.Theversionofthepropertyasadesirablebehaviorcouldbeasfollows: Move: []((reqL&&posU)-><>posBelowU), thepropositionsintheformulaaredefinedusingmacroslikeFLR_EQunderorFLR_LTunderthatimplementthe(classic)underapproximatedtestαu.Itisworthrecallingthat,asdiscussedinSect.4.4,spinautomaticallynegatesthepropositionsoftheformulaandtransformstheireval-uationintotheoverapproximatedversiontointernallyrefutethenegatedformulaagainsttheabstractmodel.However,allthisprocessistransparentfortheuser. Nowtheverificationresultfortheabstractformulais“valid”,whichensures(usingTheorem1)thatthecon-cretemodelsatisfiestheproperty.Again,thebenefitsofverifyingwiththismethodareshowninTable1andFig.19. 5.4Usingrefinement AsexplainedinSect.4.5,theabstractionusuallyintro-ducesspurioustracesthatcanpreventtheverificationofproperties.Inthatsection,themannerinwhichthesetracescansometimesberemovedinasafewaywasalsoexplained.Nowwedealwithoneofthemosttypicalcases:theadditionofnonprogresscyclesintheabstractmodel. Anonprogresscycledoesnotcontaininstructionsla-belledas“progressinstructions”.Itusuallycorrespondstononrealisticexecutionsduetoanonfairschedulingmechanism.Thelabelsinthecodeareusedtoindicatewhetherthesystemisworkingtoproducerealevolution.Forexample,thelabelprogress_requestinFig.8isusedtoexpressthatourmodelworksproperlyifweal-wayshaverequests. Checkingtheabsenceofthesecyclescanbedonedirectlyusingspin.However,itcanalsobedonecheck-ingthatthetemporalformula<>!(np_)issatisfiedbyallexecutionpaths,wheretheBooleanvariablenp_ wherereqLrepresentsrequestsfromLower.PropositionsposUandposBelowUindicatewhethertheliftiscurrentlyatorbelowtheupperfloor.Again,thenewpropositionsaredefinedbytheuserwiththestandardinterpretation: #defineposBelowU (Position[0]<(nb_floor-1)). Ifwewanttoemployabstractionwhenselectingdesiredbehavior(PropertyholdsforAllExecutions),themodelistransformedasintherefutationcase.How-ever,theformulaisnowunderapproximated.Notethat M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking181 isaninternalvariablethatistrueinastateifthatstatebelongstoanonprogresscycle.Usingeitherofthesetwomethods,itiseasytocheckthatthecon-cretemodelemployedinthepreviousexperimentsneverproducesnonprogresscycles.Butwecannotsaythesameaboutitsabstractversion(partiallyshowninFig.18). TheprobleminFig.18arisesintheevaluationofFLR_LT(f,FLR_Map(FLR_LOW,FLR_HIGH,(nb_floor-1))todecidewhethertoincreasethevariablef.Theequiva-lenttestneverproducesacycleintheconcretemodel.ButtheoverapproximationofFLR_LTmakesthetesttruewhen,forexample,ftakesthevalueNoLower.AsFLR_INC(NoLower)returnsNoLower,thecycleisproduced. Thenonprogresscycleintheabstractmodelpro-ducestheviolationofasimpleuniversalpropertylike<>posAboveL.FollowingSect.4.5,wecanemployarefinerformulatodiscardnonprogressabstracttracesinordertocheckthedesiredformula.Thecompleteformulatobecheckedisthefollowing: <> progress-> <>posAboveL #defineposAboveL FLR_GTunder(Position[0],FLR_Map(FLR_LOW,FLR_HIGH,0)) #defineprogress!(np_). Thiskindofrefiner(<>progress)hasprovedtobeveryusefulforrealisticabstractions.6Implementationnotes Thelackoftoolssupportingautomaticabstractioncouldbeduetothegreateffortneededtodevelopthem.Takingthisfactintoaccount,amaindesigncriterionintheim-plementationofourabstractiontoolistoobtainasmuchreusablecodeforothermodellinglanguagesandmodelcheckersaspossible.Inthisway,wecanapplythesametransformationapproachtoothermodellinglanguages Fig.19.Verificationresults withlesseffort.Forthisreasonweconsiderxmlastheuniqueinternalrepresentationtoperformtheabstrac-tionbytransformationasshowninFig.20forαspin.The proctypeSampler(){ mtypef=FLR_Map(FLR_LOW,FLR_HIGH,0);do ::f=Position[0]-> .... do/*Choosethefloortorequest*/ ::(FLR_LT(f,FLR_Map(FLR_LOW,FLR_HIGH,(nb_floor-1))) &&FLR_NE(f,Position[0]))->FLR_INCR(f) ::breakod; progress_request: ARRAY_SET(internal_request,f,1); .....od} Fig.18.PartofabstractversionofSampler() 182M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking actualmodellinglanguage(promela)canbetranslatedintothisrepresentationbyafront-endmodule(steps1and2inFig.20),andthefinalabstractedmodelforthemodelcheckercanbeproducedbyaspecificback-endmodule(steps6and7).Figure20containsxspinbe-causewehaveextendedthisGUItostarttheabstrac-tionmoduleasanewoptimizationoptionforverification.Themodifiedxspinalsosupportstheautomaticsyntac-tictransformationoftemporalformulas. Asregardsabstractionfunctions,xmlisapowerfulmeansofrepresentingthemappingbetweenconcreteandabstractdataandabstractoperations,includingdetailssuchasthetypeofoperands,associativityrules,etc.Fur-thermore,thewholeabstractionlibrarycanbedefinedasanxmlrepository.Thus,ifweusethesameinternalno-tationforbothmodelsandabstractionfunctions,wecanconcentrateeffortsondevelopingreusabletechniquesanduniformtoolsfortransformation-basedabstraction[19].Itisworthnotingthattheinternalxmlformatmaybedifferentforeverymodellinglanguage,butthecodewrittentomanipulatethisinternalrepresentationcouldbereused,savingtimecomparedwiththeuseofmoreadhocapproaches.ThisideahasbeensuccessfullyfollowedbyGondowandKawashimaforaverysimilartasklikeslicing[27]. Currently,αspinisthefirstresultwiththisap-proach.However,thereisworkinprogresstodealwith Fig.20.Architectureofxmlbasedabstractionandmodulesof αspin theabstractionproblemforSDL[17]andUMLState-Charts[20]. ThecurrentimplementationiswritteninJava,anditiscomposedofthemodulesshowninFig.20.Wearestillworkingontheabstractionproverthatwillassistingen-eratingnewcorrectabstractionfunctionstobeincludedinthelibrary.7Conclusions Themaincontributionofthispaperisthepresentationofatooltoperformabstractionbysyntactictransform-ationinthecontextofexplicitmodelchecking.αspinintegratestheclassicmethodforabstractingtemporallogicandthedualoverapproximationmethod.Asfarasweknow,αspinistheonlyworkingtooltoimplementab-stractionforpromela.Althoughthereareotherpropos-alstoabstractthislanguage,theyarenotimplementedornotautomatic.Perhaps[15]isthemostrepresentativeworkinthiscontext. Thetheoreticalapproachthatsupportsthetrans-formationgivesusasafeframeworkinwhichtorelatetheresultsintheabstractandtheconcretemodels(andformulas).Wearenowapplyingthistheoreticalframe-worktoextendothermodelcheckerswithabstraction-by-transformationcapabilities[17,20]. Otherinterestingcontributionsaretheuseofabstrac-tionlibrariesandtheuseofxmltosupporttheabstrac-tionprocess.Thelibraryshouldbeemployedtostorenewfunctionsthatarerevealedasusefulintheverificationexperiences.Itisevenpossibletoassignataxonomytothesefunctionstomaketheiruseeasier(Graf2002,per-sonalcommunication).Again,xmlisagoodcandidatetostorethisinformation. Onefutureprojectistoaddstrategiestoautomat-icallyanalyzethecorrectnessofabstractionfunctionsusingPVS.Anotherlineofworkistointegratemethodsforcounterexampleanalysis[6]. Documentationandcurrentandfutureversionsofαspincanbefoundat[46]. Acknowledgements.Thanksareduetotheanonymousrefereesfortheirsuggestionsandcarefulreadingofthispaper. References 1.BallT,PodelskiA,RajamaniS(2001)BooleanandCartesianabstractionsformodelcheckingCprograms.In:ProceedingsofTACAS01,Genova,Italy,2–6April2001.Lecturenotesincomputerscience,vol2031.Springer,BerlinHeidelbergNewYork,pp268–283 2.BallT,RajamaniSK(2002)TheSLAMproject:debuggingsystemsoftwareviastaticanalysis.In:ProceedingsofPOPL2002,Portland,OR,16–18January2002,pp1–3 3.BratG,HavelundK,ParkS,VisserW(2000)JavaPathFinder–asecondgenerationofaJavamodelchecker.In:Proceed-ingsofthePost-CAV’00workshoponadvancesinverification,Chicago,20July2000 M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking 183 4.ClarkeEM,EmersonEA,SistlaAP(1986)Automaticverifi-cationoffinite-stateconcurrentsystemsusingtemporallogicspecifications.ACMTOPLAS8(2):244–263 5.ClarkeEM,GrumbergO,LongDE(1994)Modelcheckingandabstraction.ACMTOPLAS16(5):1512–1542 6.ClarkeEM,GrumbergO,JhaS,LuY,VeithH(2000)Counterexample-guidedabstractionrefinement.In:Proceed-ingsofthe12thInternationalConferenceCAV’00,Chicago,15–19July2000.Lecturenotesincomputerscience,vol1855.Springer,BerlinHeidelbergNewYork,pp154–169 7.ClarkeE,GrumbergO,PeledD(2000)Modelchecking.MITPress,Cambridge,MA 8.CleavelandR,IyerSP,YankelevichD(1995)Optimalityandabstractioninmodelchecking.In:MycroftA(ed)Proceedingsofthesymposiumonstaticanalysis,Glasgow,25–27Septem-ber1995.Lecturenotesincomputerscience,vol983.Springer,BerlinHeidelbergNewYork,pp51–63 9.CousotP,CousotR(1977)Abstractinterpretation:aunifiedlatticemodelforstaticanalysisofprogramsbyconstructionorapproximationoffixpoints.In:Conferencerecordofthe4thACMsymposiumonPOPL,LosAngeles,January1977,pp238–252 10.DamsD,GerthR,GrumbergO(1977)Abstractinterpreta-tionofreactivesystems.ACMTOPLAS19(2):253–291 11.DamsD(2002)Abstractioninsoftwaremodelchecking:prin-ciplesandpractice.In:Proceedingsofthe9thinternationalSPINworkshop:modelcheckingsoftware,Grenoble,France,11–13April2002.Lecturenotesincomputerscience,vol2318.Springer,BerlinHeidelbergNewYork,pp14–21 12.DamsD,HesseW,HolzmannGJ(2002)AbstractingCwith abC.In:Proceedingsofthe14thinternationalconferenceCAV’02,Copenhagen,27–31July2002.Lecturenotesincom-puterscience,vol2404.Springer,BerlinHeidelbergNewYork,pp515–520 13.DuvalG,CattelT(1997)Fromarchitecturedowntoimple-mentationofsafeprocesscontrolapplications:design,verifica-tionandsimulation.In:Proceedingsofthe13thannualHawaiiinternationalconferenceonsystemsciences(HICSS30),Hon-olulu,3–6January1997 14.DwyerM,HatcliffJ,JoehanesR,LaubachS,PasareanuC, VisserW,ZhengH(2001)Tool-supportedprogramabstrac-tionforfinite-stateverification.In:ProceedingsofICSE2001,Toronto,12–19May2001,pp177–187 15.FersmanE,JonssonB(2000)Abstractionofcommunication channelsinPromela:acasestudy.In:Proceedingsofthe3rdinternationalSPINworkshop,Stanford,CA,31August–1September2000,pp187–204 16.GallardoMM,MerinoP(1999)Aframeworkforautomatic constructionofabstractpromelamodels.In:Theoreticalandpracticalaspectsofspinmodelchecking.Lecturenotesincomputerscience,vol1680.Springer,BerlinHeidelbergNewYork,pp184–199 17.GallardoMM,MerinoP(2000)Apracticalmethodtointe-grateabstractionsintoSDLandMSCbasedtools.In:Pro-ceedingsofthe5thinternationalERCIMworkshoponformalmethodsforindustrialcriticalsystems,Berlin,3–4April2000.GMDReport91,pp84–89 18.GallardoMM,MerinoP,PimentelE(2002)Verifyingabstract LTLpropertiesonconcurrentsystems.In:Proceedingsofthe6thworldconferenceonintegrateddesign&processtechnol-ogy,Pasadena,CA,23–28June2002 19.GallardoMM,MartinezJ,MerinoP,RosalesE(2002)Using XMLtoimplementabstractionformodelchecking.In:Pro-ceedingsoftheACMsymposiumonappliedcomputing,Madrid,10–12March2002,pp1021–1025 20.GallardoMM,MerinoP,PimentelE(2002)DebuggingUML designswithmodelchecking.JObjectTechnol1(2):101–11721.GallardoMM,MerinoP,PimentelE(2002)Comparing underandover-approximationsofLTLpropertiesformodelchecking.In:Proceedingsofthe11hinternationalwork-shoponfunctionaland(constraint)logicprogramming,Grado,Italy,20–22June2002.Electronicnotesintheoret-icalcomputerscience,vol76.Elsevier,Amsterdam.Avail-ableat:http://www.elsevier.nl/gej-ng/31/29/23/show/Products/notes/index.htt 22.GallardoMM,Mart´inezJ,MerinoP,PimentelE(2002)Atool forabstractioninmodelchecking.In:Proceedingsofthe7thinternationalworkshoponformalmethodsforindustrialcriti-calsystems,M´alaga,12-13July2002.Electronicnotesinthe-oreticalcomputerscience,66(2).Elsevier,Amsterdam.Avail-ableat:http://www.elsevier.nl/gej-ng/31/29/23/show/Products/notes/index.htt 23.GallardoMM,MerinoP,PimentelE(2002)RefinementofLTL formulasforabstractmodelchecking.In:Proceedingsofthe9thinternationalstaticanalysissymposium(SAS’02),Madrid,17–20September2002.Lecturenotesincomputerscience,vol2477.Springer,BerlinHeidelbergNewYork,pp395–410 24.GerthR,PeledD,VardiM,WolperP(1995)Simpleon-the-fly automaticverificationoflineartemporallogic.In:Proceedingsofthe15thworkshoponprotocolspecification,testing,andver-ification(PSTV95),Warsaw,Poland,13–16June1995,pp3–1825.GiacobazziR,RanzatoF,ScozzariF(2000)Makingabstract interpretationcomplete.JACM47(2):361–416 26.GiacobazziR,QuintarelliE(2001)Incompleteness,coun-terexamplesandrefinementinabstractmodel-checking.In:Proceedingsofthe8thinternationalstaticanalysissympo-sium(SAS’01),Paris,16–18July2001.Lecturenotesincom-puterscience,vol2126.Springer,BerlinHeidelbergNewYork,pp356–373 27.GondowK,KawashimaH(2002)TowardsANSICprogram slicingusingXML.In:Proceedingsofthe2ndworkshoponlanguagedescriptions,toolsandapplications(LDTA2002),Grenoble,France,13April2002.Electronicnotesintheor-eticalcomputerscience,vol65,no3.Elsevier,Amsterdam.Availableat:http://www.informatik.uni-trier.de/∼ley/db/journals/entcs/entcs65.html 28.GrafS(1994)Verificationofadistributedcachememoryby usingabstractions.In:Proceedingsofthe6thinternationalconferenceCAV’94,Stanford,CA,21–23June1994.Lecturenotesincomputerscience,vol818.Springer,BerlinHeidelbergNewYork,pp207–21929.GrafS,Sa¨idiH(1997)Constructionofabstractstategraphs withPVS.In:Proceedingsofthe9thinternationalconferenceCAV’97,Haifa,Israel,22–25June1997.Lecturenotesincom-puterscience,vol1254.Springer,BerlinHeidelbergNewYork,pp72–83 30.HatcliffJ,DwyerM,PasareanuC,Robby(2003)Foundations oftheBanderaabstractiontools.Theessenceofcompution.Lecturenotesincomputerscience,vol2566.Springer,BerlinHeidelbergNewYork,pp172–203 31.HavelundK,PressburgerT(2000)ModelcheckingJavapro-gramsusingJavaPathFinder.IntJSoftwToolsTechnolTransfer2(4):366–381 32.HavelundK,VisserW(2002)Programmodelcheckingas anewtrend.IntJSoftwToolsTechnolTransfer4:8–20 33.HolzmannGJ(1991)Designandvalidationofcomputerpro-tocols.Prentice-Hall,UpperSaddleRiver,NJ 34.HolzmannGJ(1997)ThemodelcheckerSPIN.IEEETrans SoftwEng23(5):279–295 35.HolzmannGJ(1999)Theengineeringofamodelchecker: theGnui-Protocolcasestudyrevisited.In:Theoreticalandpracticalaspectsofspinmodelchecking,Lecturenotesincomputerscience,vol1680.Springer,BerlinHeidelbergNewYork,pp156–168 36.HolzmannGJ,NajmE,SerhrouchniA(2000)SPINmodel checking:anintroduction.IntJSoftwToolsTechnolTransfer2:321–327 37.HolzmannGJ,SmithMH(1999)Apracticalmethodforthe verificationofeventdrivensystems.In:Proceedingsof21stIn-ternationalConferenceonSoftwareEngineeringICSE99,LosAngeles,12–22May1999,pp597–608 38.KelbP(1994)Modelcheckingandabstraction:aframework preservingbothtruthandfailureinformation.TecnicalRe-portOFFIS,UniversityofOldenburg,Germany 39.KestenY,PnueliA(2000)Verificationbyaugmentedfinitary abstraction.InfComput(SpecialIssueonCompositionality163:203–243 40.KestenY,PnueliA(2000)Controlanddataabstraction:the cornerstonesofpracticalformalverification.IntJSoftwToolsTechnolTransfer2:328–342 184M.delMarGallardoetal.:αspin:Atoolforabstractmodelchecking 41.LoiseauxC,GrafS,SifakisJ,BouajjaniA,BensalemS(1995) Propertypreservingabstractionsfortheverificationofconcur-rentsystems.FormalMethSysDes6:1–35 42.PasareanuCS,DwyerMB,VisserW(2001)Findingfeasible counter-exampleswhenmodelcheckingabstractedJavapro-grams.In:Proceedingsofthe7thinternationalconferenceontoolsandalgorithmsfortheconstructionandanalysisofsys-tems,(TACAS2001)Genova,2–6April2001.Lecturenotesincomputerscience,vol2031,Springer,BerlinHeidelbergNewYork,pp284–29843.Sa¨ıdiH(2000)Modelcheckingguidedabstractionandan-alysis.In:Proceedingsofthe7thinternationalstaticanalysis symposium(SAS2000),SantaBarbara,29June–1July2000.Lecturenotesincomputerscience,vol1824.Springer,BerlinHeidelbergNewYork,pp377–396 44.VisserW,HavelundK,BratG,ParkS(2000)Modelcheck-ingprograms.In:Proceedingsofthe15thIEEEconferenceonautomatedsoftwareengineering,Grenoble,France,11–15September2000,pp3–12 45.W3Consortium.ExtensibleMarkupLanguage(XML)1.0,2nd edn.Availableat:http://www.w3.org/XML/46.αspinproject.UniversityofM´alaga. http://www.lcc.uma.es/gisum/fmse/tools Appendix:Electronicappendix Thefollowingfilesrelatedtothispaperareavailableelec-tronically: Currentinstallableversionofαspin: http://www.lcc.uma.es/gisum/fmse/tools/stuff/aspin09.exe Concreteandabstractversionsoftheliftcontroller: http://www.lcc.uma.es/gisum/fmse/tools/stuff/lift.zip 因篇幅问题不能全部显示，请点此查看更多更全内容