over-approximation.ppt

GoingfromConcretetoSymbolicModelCheckingviaPredicateAbstraction WillemVisserCorinaPasareanuandRadekPelanekAutomatedSoftwareEngineeringGroupNASAAmesResearchCenter Overview AbstractionClassicover approximationbasedCounter examplebasedrefinementUnder approximationbasedRefinementbasedonabstraction sexactnessLightweightframeworkfortestingTestgenerationenvironmentbuiltaroundJPFwithsymbolicexecutionMeasurepredicatecoverageEvaluateagainstothertest casegenerationmethodsJavaContainerclasses PredicateAbstraction AbstractionMapping Fora a in2 preds ifwp a T aaddtransitiona a maytransition musttransition ExampleAbstraction wp p x x 1 paddp p wp p x x 1 p x 1 0 x x 1 p wp p x x 1 paddp p x 1 0 x x 1 p wp p x x 1 padd p p p wp p x x 1 p pismusttrans Refinement 1 p T 2 while p 3 p p F T F 4 assertfalse InfeasibleCounterExample1 2 3 F 2 4 1 x 2 x 0 2 x 2 x 0 3 x 1 x 0 x 1 x x 1 x 0 must may Let sGoOutsidetheBox Ratherthanover approximateandrefine weunder approximateandrefineClearlycomplementsexistingtechniquesIfwerestrictourselvesonlytofeasiblebehaviorswhenunder approximatingthenallsafetypropertyviolationswillbepreservedBuildontopofclassicexplicit statemodelcheckinginfrastructure ClassicExplicit StateSearch PROCEDUREdfs s top Stack FORalltransitionstenabledinsDOs successor s afterexecutingt IFs NOTINVisitedStatesTHENEnters intoVisitedStates Pushs ontoStack dfs ENDEND PopsfromStack INIT Enters0intoVisitedStates Pushs0ontoStack dfs Explicit State 1 step Search PROCEDUREdfs s top Stack FORalltransitionstenabledinsDOs successor s afterexecutingt IF s NOTINVisitedStatesTHENEnter s intoVisitedStates Pushs ontoStack dfs ENDEND PopsfromStack INIT Enter s0 intoVisitedStates Pushs0ontoStack dfs Search 1 x 2 2 while x 0 3 x x 1 4 assertfalse AbstractionMappingp x 0 Mapconcretestatestoabstractstatesforstatestoring Alwaystraverseonlyfeasiblepaths Under approximationofthebehaviors Concrete May Must Concrete C 0 E 2 B 1 Concrete Search A 0 D 1 D 0 AbstractionSearchp x 2 Refinement Search A 0 D 1 D 0 E 1 E 2 B 1 C 0 Example 1 x 2 2 while x 0 3 x x 1 4 assertfalse AbstractionMappingp x 0 Refinement Checkiftheinducedabstracttransitionisamusttransition Ifnot addnewpredicates Addx 1toabstractionpredicatesandrepeatsearchGloballyforalltransitionsLocallyonlyforthetransition location itrefines PredicateAbstraction Search ShowingpropertyholdsOver approximationbasedCounter exampledrivenrefinementExpensivecomputationtocalculateabstraction FindingdefectsUnder approximationbasedAbstractiondrivenrefinementTrivialcomputationtocalculateabstractionmapping Issue reachable unreachable T wp p T p ifnewpredicatesareinfinitelyrequiredtorefinetheunreachableareathealgorithmwillnotterminate Example x 0 y 0 while y 0 y x y Therefinementonlyrefinestheunreachablestatespace ModifiedBakery whiletrue x y x x 1 wait x y x 0 whiletrue y x y y 1 wait y x y 0 SearchOrderMatters SymbolicExecutionand Search CurrentimplementationisforasimpleinputlanguageoCamlusingSimplifyasadecisionprocedureWewouldliketointegratethetechniqueinJavaPathfinder JPF thatsupportssymbolicexecution usingtheOmegaLibrary Toallowapplicationtoprogramswithcomplexdatastructures objects FromConcretetoSymbolic X 1 Y 0 ConcreteBehavior X Y SymbolicBehavior PossibleApproach ExecutetheconcreteprogramonvalidinputsCollectallpredicatesinpathconditionSolveconstraintsoverallcombinationsofthesepredicatesUseresultsasinputsforstep1Whennonewpredicatesarefound or ifanerrorisfound terminate Example publicstaticvoidmethod intx inty if x 0 y0 else method 1 1 true method 1 1 p1 p2 Example 2 publicstaticvoidmethod intx inty if x 0 y0 else method 1 6 p1 p2 x 0 y 10 y 5 end method 1 6 p1 p2 Example 4 publicstaticvoidmethod intx inty if x 0 y0 else method 1 1 p1 p2 x 0 y 10 x 0 end method 1 1 p1 p2 p3 p1 p3 method 1 11 SolveConstraints Example 3 publicstaticvoidmethod intx inty if x 0 y0 else method 1 11 p1 p3 method 1 11 p1 p3 x 0 y 10 x 0 end EndofPartOne Showedunder approximationbasedsearchwithrefinementBackwardweakestpreconditionbasedForwardsymbolicexecutionbasedPartTwoRatherthanautomatedrefinementweuseuser providedabstractionsMotivationistogeneratetest casestoachievehighbehavioralcoverageforJavacontainerclasses Explicit State 1 step Search PROCEDUREdfs s top Stack FORalltransitionstenabledinsDOs successor s afterexecutingt IF s NOTINVisitedStatesTHENEnter s intoVisitedStates Pushs ontoStack dfs ENDEND PopsfromStack INIT Enter s0 intoVisitedStates Pushs0ontoStack dfs GeneralIdea SUT ENV m n mistheseq lengthofAPIcalls nisthenumberofvaluesusedintheparametersofthecalls API put v del v Evaluatedifferenttechniquesforselectingtest casesfromENV m n toobtainmaximumcoverage PredicateCoverage Coverallcombinationsofagivensetofpredicatesateachbranchinthecode Red BlackTreePredicatesroot null e left null e right null e parent null e color BLACK TechniquesConsidered RandomselectionClassicmodelcheckingStatematchingoncompletestateAbstractionsearchStatematchingonabstract partial stateSymbolicExecutionCompletematchingusingsubsumptionchecksAbstractmatching Framework SUTwithminorinstrumentation ENV TestListener AbstractionMapping StateStorage CoverageManager JPF SampleOutput Testcasenumber77for 15 L R P REDroot put 0 put 4 put 5 put 1 put 2 put 3 remove 4 UniqueIDforthetest BranchNumber PredicateValues Test casetoachieveabovecoverage EnvironmentSkeleton M sequencelengthN parametervaluesA abstractionusedfor inti 0 i M i intx Verify random N 1 switch Verify random 1 case0 put x break case1 remove x break Verify ignoreIf checkAbstractState A SymbolicEnvironmentSkeleton M sequencelengthA abstractionusedfor inti 0 i M i SymbolicIntegerx newSymbolicInteger X i switch Verify random 1 case0 put x break case1 remove x break Verify ignoreIf checkAbstractState A AbstractionSearch Mapstatetoanabstractversionandbacktrackiftheabstractstatewasseenbefore i e discardtest caseMappingcanbelossyornotAbstractionmappingscanbecreatedbytheuser testerDefaultabstractionmappingsareprovided DefaultMappings Structureoftheheapoftheprograme g structureofthecontainersStructureaugmentedwithnon datafieldsStructureaugmentedwithsymbolicconstraintsonthedatainthestructureThisrequirescheckingconstraintsubsumption LinearizationComparingStructures 1 2 3 4 5 1 2 3 4 5 1 2 3 4 5 1 2 3 4 5 123 1 14 1 15 1 1 123 1 14 1 15 1 1 123 1 14 1 15 1 1 123 1 14 15 1 1 1 4 3 2 1 Linearization Mapping 1 2 3 4 5 1b2b3r 1 14r 1 15b 1 1 5 1b2r3r 1 14r 1 15r 1 1 Linearizationtakesamappingobjectasparametertoindicatehoweachnodeintheheapshouldbelinearized Intheexampleaboveeachnodegets besidestheuniqueidentifier amappingof r iftheoriginalstructurehadarednodeand b iftheoriginalstructurehadablacknodeinthatposition Ifwealsoaddedthekeyvaluesforeachnodethelinearizationmighthavelookedsomethinglike 1b62b43r3 1 14r5 1 15b7 1 1 SymbolicExecution SymbolicState x1 x2 x3 x4 x5 x1 x2 x2 x3 x2x1 Shape SymbolicConstraints SubsumptionChecking x1 x2 x3 x4 x5 x1 x2 x2 x3 x2x1 x1 x2 x3 x4 x5 x1 x2 x2 x3 x2x1 Ifonlyitwasthissimple GettingReadyforCheckingExistentialElimination x1 x2 x3 x4 x5 PCs1s3 s4s1 s1 s4 s2 s3 s5 s1 s2 s3 s4 s5suchthatx1 s1 x2 s4 x3 s3 x4 s5 x5 s2 PC x1 x2 x2 x3 x2x1 CheckingSubsumption newstate C1 C2 oldstate C1 C2 Checknew old new old isunsatisfiable new old new old C1 C2 C1 C2 C1 C2 C1 C1 C2 C2 Oops NegationandOrdoesn tworkinourversionoftheOmegaLib BidirectionalSubsumptionChecking Ifnew oldbacktrackIfold newnewismoregeneralthanoldreplaceoldwithnewtoincreasechancesofgettingamatchinthefutureContinueonpathfromnew i e don tbacktrackUltimatelyforeachshapewewanttousedisjunctionofconstraintsSmalltechnicalitypreventsus buginomegalib Evaluation Red BlackTreesOutofMemoryrunsarenotreportedBreadth firstSearchunlessstatedSequenceLength Valuesforthenon symbolicsearchesFirstcompareunderBranchCoverage ExhaustiveTechniquesBranchCoverage OptimalBranchCoverageis39 Under ApproximationTechniquesBranchCoverage OptimalBranchCoverageis39 ExhaustiveTechniquesPredicateCoverage OptimalPredicateCoverageis106 Under ApproximationTechniquesPredicateCoverage OptimalPredicateCoverageis106 Observations Forasimplecoveragesuchasbranchcoverage allthetechniquesworkwell includingtheexhaustiveonesButmakingthecoveragemore behavioral evenbyasmallincrement killsofftheexhaustivetechniques Observations FullBlownModelCheckingdoesn tworkhereItsclosecousin thatonlylooksattherelevantstateattherelevanttime scalesmuchbetterBranch fullcoverageafter MC 536s 584MbComplete 10s 17MbPredicate bestcoverageafter MC 79coveredwith543s 309MbComplete 95coveredwith350s 228Mb Observations SymbolictechniqueshaveaslightedgeoverconcreteonesforexhaustiveanalysisComparingforPredicateCoverage 10 FullConcrete