Measuring Progress of Java PathFinder
Java PathFinder (JPF for short) is an explicit-state model-checker
for Java bytecode. JPF is generally not suitable for verifying
implementations of randomized algorithms. Recently, we developed
a theoretical framework to measure the amount of progress an
explicit-state probabilistic model-checker has made with its verification
effort. The details of our proposed framework can be found in
this paper.
We have implemented this framework within JPF. A discussion of our
implementation can be found in
this paper.
To exploit our extension of JPF to keep track of its progress when
model-checking an implementation of a randomized algorithm,
All the above should be added to the classpath. Furthermore, configure
JPF in such a way that it keeps track of the progress. To change the
configuration of JPF from the default, change the jpf.properties
file which can be found in the JPF root directory. JPF loads the properties
from the jpf.properties file and changes its configuration
accordingly. In order for JPF to keep track of its progress,
the jpf.listener property has to be set to
ProbabilityListener in the jpf.properties file as follows.
jpf.listener = probabilistic.ProbabilityListener
To use one of the new search strategies (probability-first search (PFS) or
breadth-first probability-second search (BFPSS)), specify that in the
jpf.properties file as well. For example, to use PFS, the
search.class property has to be set to PFS in
the jpf.properties file as follows.
search.class = gov.nasa.jpf.search.PFS
