F. Model checking software at compile time(10)

4.3PropertyImplementationinGoanna

4.2ModelCheckingwithNuSMV

PartsoftheNuSMVcoderesultingfromthetranslationofthelabelledCFGareshowninFigure4.AsdescribedinSection3.3weintroduceoneenumeratedtypevariable,i.e.,location,rangingoverthecontrollocations(i.e.thenodesintheCFG),describethetransitionrelationasasetoftransitionsfromlocationstoasetoflocations,anduseDEFINEdeclarationstoassociatelabelstocertainloca-tions.Notethat,forclarityofpresentation,weusetheweakuntiloperandWintheCTLspeci cation,whichdoesnotex-istinNuSMVsyntax,butcanbeequallyexpressedthroughotherexistingoperators.

UsingNuSMVforcheckingproperty(1)(describedinSection3.1)ontheannotatedCFGnowrevealsaviolationoftheNuSMVspeci cationfromFigure4.GoannaautomaticallyexaminestheviolationreportedbyNuSMVandconcludesthatthereisanincorrectuseofvariablea—infact,thereisapathintheprogram

6

InordertoimplementsuchapropertyinourGoannatool,weonlyneedtoidentifythenodesofinterest(asde-scribedinSection4.1),describetheirrelationshipsinCTLformulasandprinttheseformulasinNuSMVsyntaxtoNuSMV’sinput le(asdescribedinSubsection4.2).AnimplementationofourexamplepropertyisshowninpseudocodeinFigure5.Inthecode,we rst ndthesetofallvariablesthataredeclaredinafunction,becausethesearetheonesthatneedtobecheckedforproperinitialization.Foreachofthesevariables,wethenprinttheCTLspeci -cationstotheNuSMVinput le(thefunctionNuSMV()simplyprintstexttoNuSMV’sinput le).Inthenextstep,foreveryvariableinthesetofdeclaredvariables,wesearchforthesetofnodesintheASTwherethevariableisassignedavalueandwhereitisused,respectively.ForthissearchweusethefunctionFindAST()thatidenti- esnodesintheASTaccordingtospeci cpatterns.Fi-nally,fromthesethreesets,wegetthecorrespondingsetsoflocationsoftherespectivenodesintheCFGbyusingthefunctionCFGlocations().Thatfunctiontranslates

搜索“diyifanwen.net”或“第一范文网”即可找到本站免费阅读全部范文。收藏本站方便下次阅读，第一范文网，提供最新高等教育F. Model checking software at compile time(10)全文阅读和word下载服务。