F. Model checking software at compile time(12)

5.3

Run-timePerformanceandMemoryUsage

First,welookatsomeoverallperformancenumbers.Wemeasurethewall-clockcompiletimeandcompareitwithGoanna’stotalanalysistime.Furthermore,wemeasurethemaximuminternalmemoryconsumptionofourtoolaswellasNuSMV’smemoryconsumptionduringtheanalysis.Theresultsforonepropertyandforall15propertiesareshowninTable1.Itshowsthattheoverallanalysistimeiswellwithinthesameorderofmagnitudeasthecompile

1/