© 2007 Carnegie Mellon UniversityIntroduction to JavaPathfinderPart 1Software Engineering InstituteCarnegie Mellon UniversityPittsburgh, PA 15213Sagar Chaki20 November 20072Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityOutlineOverview of JavaPathFinderTool Description (i.e., usage)ExampleHow it works •Architecture•Specifying properties•Modeling environmentSome slides borrowed from JavaPathFinder tutorial at ASE conference 2006•http://www.visserhome.com/willem/presentations/ase06jpftut.ppt3Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityOverview4Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityWhat is JavaPathFinder (1)Explicit state model checker for Java bytecodeUses a customized Virtual Machine with backtracking capability to efficiently search a Java program’s statespaceFocus is on finding bugs in Java programs•concurrency related: deadlocks, (races), missed signals etc.•Java runtime related: unhandled exceptions, heap usage, (cycle budgets)•but also: complex application specific assertions5Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityWhat is JavaPathFinder (2)Goal is to avoid modeling effort (check the real program), or at least use a real programming language for complex modelsImplies that the main challenge is scalabilityJPF uses a variety of scalability enhancing mechanisms•user extensible state abstraction & matching•on-the-fly partial order reduction•configurable search strategies: "find the bug before you run out of memory"•user definable heuristics (searches, choice generators)Key issue is configurable extensibility: overcome scalability constraints with suitable customization (using heuristics)6Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityKey PointsModels can be infinite state•Unbounded objects, threads,…•Depth-first state generation (explicit-state)•Verification requires abstractionHandle full Java language•but only for closed systems•cannot directly handle native code—no Input/output through GUIs, files, Networks, …—Must be modeled by java code instead Allows Nondeterministic Environments•JPF traps special nondeterministic methodsChecks for User-defined assertions, deadlock and user-specified properties7Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityJPF StatusDeveloped at the Robust Software Engineering Group at NASA Ames Research CenterCurrently in it’s fourth development cycle•v1: Spin/Promela translator - 1999•v2: backtrackable, state matching JVM - 2000•v3: extension infrastructure (listeners, MJI) - 2004•v4: symbolic execution, choice generators - 4Q 2005Open sourced since 04/2005 under NOSA 1.3 license:<javapathfinder.sourceforge.net>It’s a first: no NASA system development hosted on public site before11100 downloads since publication 04/20058Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityTool Description: Usage9Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityUsing JavaPathfinderIntended to be a drop-in replacement for java, the Java VM•Thus, JPF accepts Java class files as inputTypically verify Java sources files in two steps:1.Compile .java file(s) to .class file(s) using javac2.Run JPF on the .class file(s)Command line interface•Can run JPF within Eclipse, but output is still textual, i.e., no GUI-based counterexample viewer like CBMC10Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityExamples11Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityCounterint i = 0;while (i < 2)i++;assert(i == 2);12Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityCounteri = 0int i = 0;while (i < 2)i++;assert(i == 2);13Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityCounteri = 0int i = 0;while (i < 2)i++;assert(i == 2);14Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityCounteri = 1int i = 0;while (i < 2)i++;assert(i == 2);15Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityCounteri = 1int i = 0;while (i < 2)i++;assert(i == 2);16Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityCounteri = 2int i = 0;while (i < 2)i++;assert(i == 2);17Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityCounteri = 2int i = 0;while (i < 2)i++;assert(i == 2);18Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityChoiceint x = -1,y = -1;boolean choice = Verify.getBoolean();if(choice)y = 1;assert(x == y);19Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityChoicex =-1y = -1int x = -1,y = -1;boolean choice = Verify.getBoolean();if(choice)y = 1;assert(x == y);20Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityChoicex =-1y = -1choice = falseint x = -1,y = -1;boolean choice = Verify.getBoolean();if(choice)y = 1;assert(x == y);21Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityChoicex =-1y = -1choice = falseint x = -1,y = -1;boolean choice = Verify.getBoolean();if(choice)y = 1;assert(x == y);backtrack22Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityChoicex =-1y = -1int x = -1,y = -1;boolean choice = Verify.getBoolean();if(choice)y = 1;assert(x == y);23Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityChoicex =-1y = -1choice = trueint x = -1,y = -1;boolean choice = Verify.getBoolean();if(choice)y = 1;assert(x == y);24Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityChoicex =-1y = -1choice = trueint x = -1,y = -1;boolean choice = Verify.getBoolean();if(choice)y = 1;assert(x == y);25Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityChoicex =-1y = 1choice = trueint x = -1,y = -1;boolean choice = Verify.getBoolean();if(choice)y = 1;assert(x == y);26Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityDining PhilosophersDeadlock27Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityHow it Works: Architecture28Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityJavaPathFinder Architecture29Intro to JPF: Part 1Sagar Chaki, 20 Nov 07© 2007 Carnegie Mellon UniversityUnder the Hood: Toplevel StructureTwo major concepts: Search and VMSearch is the
View Full Document