DOC PREVIEW
CMU CS 15414 - Introduction to JavaPathfinder

This preview shows page 1-2-3-19-20-38-39-40 out of 40 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

© 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

CMU CS 15414 - Introduction to JavaPathfinder

Download Introduction to JavaPathfinder
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Introduction to JavaPathfinder and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Introduction to JavaPathfinder 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?