F. Model checking software at compile time(15)

5.4ScalabilityandPrecision

Oneoftheencouragingresultsofourcasestudyisthatperformancescalesnicelywhenaddingmoreproperties.Infact,goingfromonepropertyto15propertiesonlydoublestheanalysistime.Withanoptimizedtreematching,weex-pecttofurtherimprovethisratio.

Therearetwomainreasonsforthis:Someofthelabelscreatedforcertainpropertiescanbereused.E.g.,thelabelforavariablexbeingdeclared(declx)mightbepartofsev-eralpropertiesandassuchcanbereused.Rightnow,weonlydothistoalimitedextendinGoanna.

TheotherreasonisthatNuSMVscaleswellwhenaddingmorelabels.Sincetheunderlyingcontrolstructureforonepropertyand15propertiesisthesame—onlythenumberoflabelsincreases—itisnotrequiredtorunNuSMVmoreoftenforalargernumberofproperties.Again,forreasonsoftheexactBDDencoding,itissometimesdif culttopre-ciselypredicthowlargeanincreaseinrun-timecanbeex-pectedbyaddingacertainnumberofproperties/labels.Theprecisionofouranalysisisverymuchdependentontheexactpropertyencoding.Someofourpropertiescomeintwo avors:Astrictversionandarelaxedversion.Thestrictversiontendstobeanunder-approximationofthepro-gram’sbehaviorandtherelaxedoneanover-approximation.Inthecaseofuninitializedvariables,thestrictversion agsaviolationifavariableisuninitializedonallpathsandtherelaxedversionreportsaviolationifthevariableisuninitial-izedonsomepath.Thedifferenceisinthepathquanti eroftheCTLformula(forall/existsapath).

Thestrictversionstypicallycreatezerofalsealarms,whiletherelaxedversionsarecomparabletootherstaticanalysistoolswhichdonotdoanyadditionalpathpruningorsimilartechniquestoremoveimpossiblepaths.

References

[1]T.BallandS.K.Rajamani.TheSLAMToolkit.InIntl.

Conf.onComputerAidedVeri cation(CAV’01),pages260–264,London,UK,2001.Springer-Verlag.

[2]M.Benedikt,W.Fan,andG.M.Kuper.Structuralproperties

ofxpathfragments.InICDT’03:Proceedingsofthe9thInternationalConferenceonDatabaseTheory,pages79–95,London,UK,2002.Springer-Verlag.

[3]B.Blanchet,P.Cousot,R.Cousot,J.Feret,L.Mauborgne,

A.Min´e;,D.Monniaux,andX.Rival.Designandimple-mentationofaspecial-purposestaticprogramanalyzerforsafety-criticalreal-timeembeddedsoftware.pages85–108,2002.

[4]S.Chaki,E.M.Clarke,A.Groce,andO.Strichman.Pred-icateAbstractionwithMinimumPredicates.InCHARME,pages19–34,2003.

[5]B.Chess.Improvingcomputersecurityusingextendedsta-ticchecking.InSP’02:2002IEEESymposiumonSecurityandPrivacy,page160,Washington,DC,USA,2002.IEEEComputerSociety.

6FutureWorkandConclusions

Summary.Inthisworkwepresentedanapproachtousemodelcheckingforsolvingstaticanalysisproblems.More-over,weimplementedGoanna,the rsttoolthatusesanoff-the-shelfmodelcheckerasastaticanalysisengine.Thisbringsthetwoworldsofstaticanalysisandmodelcheckingonestepclosertogether.Webelievethatinthefuturethiswillenabletheintegrationofmoresemantic-basedsoftwaremodelcheckingtechniquesintostaticanalysiswhileretain-ingoneuniformframework.

Theapproachhasbeenshowntobescalabletoreal-lifesoftwareprojects.Weevaluatedourprototypetoolwithre-specttoOpenSSLandshowedthatmost lesareanalyzedinthesameorderofmagnitudeasthecompilationitself.

9

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