F. Model checking software at compile time(13)

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analy

OpenSSL(15properties)[min:sec]

3:07[min:sec]

6:19

[MB]35.4

[min:sec]

5:54

[MB]17.9

[min:sec][MB]

12:1353.3

piletime,run-timeandmaximummemoryusageforGoannaandNuSMVseparately,

andforthewholetoolchainin

total.

807060

807060

Run time [s]

Run time [s]

504030201000

500

1000

1500

2000

2500

3000

Input file size [LoC]

50403020100

500

1000

1500

2000

2500

3000

Input file size [LoC]

Figure6.Run-timesofNuSMVwithrespecttosizeofinputsource les.

Figure7.Run-timesofthewholeGoannatoolchainwithrespecttosizeofinputsource les.

time.Infact,itistwiceaslongasthecompilationforonepropertyandfourtimesaslongfor15properties.

Moreover,fortheanalysiswithall15properties,outof602source les,only3.6%tooklongerthan2secondstoanalyzeand99.2%ofall leswereanalyzedinlessthan5seconds.ThetimespentinNuSMVismostlynegligiblewith98.7%ofall lesbeinganalyzedinlessthen2seconds.Theoveralldistributionoftheruntimewithrespecttothe lesizeisshowninFigure6forNuSMVandinFig-ure7fortheoverallanalysistime.Notethatthecomplexityoftheanalysis—andhenceitsruntime—doesnotperfectlycorrelatewiththe lesize,butthe lesizeiseasilyunder-standableandtypicallyameasureofinteresttothedevel-oper.Infact,thecomplexityofourcurrentimplementationismostlydependentonthenumberofvariablesandthesizeoftheCFG.

Thememoryconsumptionforoneaswellasfor15prop-ertieshasbeenconsiderablylowwith35.3and53.3MB,respectively.This tswellintothestandardmemoryofastate-of-the-artmachine,makingthisapproachwellsuitedtobeintegratedintothestandardbuildprocessonadevel-oper’sdesktop

machine.

8

Discussion.ThereareacoupleofpathologicalcaseswhereNuSMVtakesdisproportionallylongandsomewhereGoanna,i.e.,thetreematching,takesverylong.Therearetwosometimesinterrelatedreasonsforthis:Firstofall,Goanna’streematchingisimpactedbythenumberofvariablesinaprogram.Thecurrentimplementationrunsallmatchingoperationsforallpropertiesandallvariablesinseparateruns,creatingaratherlargeoverhead.Forpro-gramswithfewvariables,theimpactisnotsigni cant,how-ever,whenanalyzinghundredsofvariablesitisconsider-able.AnexampleofthiseffectcanbeseeninFigure7,wheretheoutlinerwith70secondsrun-timeiscausedbyasource lethathasalargenumberofvariables.Conse-quently,wehaveplanstooptimizethetreematchinginthefuture.

Secondly,NuSMVisimpactedbythenumberofvari-ablesandthecomplexityofthecontrolstructure.More-over,theBDDencodingplaysamajorrole.AsistypicalinBDD-basedmodelchecking,run-timesaresometimeshardtopredictand uctuatewildlywhenchangingthevariableorder.Anexplicitstatemodelcheckermightbemoresuit-