Java Pathfinder is a system to verify executable Java bytecode programs. In its basic form, it is a Java Virtual Machine (JVM) that is used as an explicit state software model checker developed by NASA.

An Example about Path Finding

Below a small example for detecting a possible bug (assert) in a control flow:

int x, y;

if (x > y) {
x = x + y;
y = x – y;
x = x – y;
if (x > y)
assert false;
}
Below its logic is drawn:

Java Path Finder is able to follow on paths and to evaluate expressions using symbolic evaluation.

JPF is rather flexible

  • Symbolic execution
  • Can start at any point in the program
  • Can use mixed symbolic and concrete inputs
  • No special test driver needed – sufficient to have an executable program that uses the method/code under test

  • Any time symbolic execution
  • Use specialized listener to monitor concrete execution and trigger symbolic execution based on certain conditions
  • Unit level analysis in realistic contexts
  • Use concrete system-level execution to set-up environment for unit-level symbolic analysis
  • Applications:
  • Exercise deep system executions
  • Extend/modify existing tests: e.g. test sequence generation for Java containers

Inside JPF

JPF is an extension to  JVM. JPF Listener is able to listen code execution.

Symbolic Analysis (SAM) vs. JPF

SAM has not initially been planned for evaluating paths, because its main function is deterministic. However, its symbolic model allows traversing multiple paths at the same time. In that nondeterm mode, it should write its intermediate results to a tape tree, which is a modification from a standard trace (see Turing machine: tape).

Starting simulation via SAM is as flexible as JPF.

Other tools

MoonWalker is a model checker developed on the Mono platform. MoonWalker is a program to automatically detect errors in CIL bytecode programs, i.e. applications written for the .NET platform.

The current version of MoonWalker is able to find deadlocks and assertion violations in CIL programs, generated with Mono’s C# compiler.

Some links:

Advertisements