How to Implement Properties

There are three general types of property checks that can be performed with JPF: (1) ordinary assertions, (2) gov.nasa.jpf.Property based, and (3) gov.nasa.jpf.SearchListener or gov.nasa.jpf.VMListener based.

(1) Java assertions inside the application under test are the most straight forward way to test simple safety properties that only depend on test application data values (e.g. parameter value intervals). Violations (AssertionErrors) are caught be JPF's generic NoUncaughtExceptionProperty. The drawback of this method is that it requires access to the test application sources, and that it can significantly increase the state space if the property requires evaluation state itself (e.g. for properties implemented as automatons)

(2) gov.nasa.jpf.Property instances are used to encapsulate property checks. These instances can be configured statically (via the search.properties setting) or dynamically (via jpf.getSearch().addProperty()), and are checked by the Search object after each transition. In case a Property.check(..) method implementation returns false, and termination has been requested, the search process is ended, and all violated properties are printed (which potentially includes error traces)

JPF comes with the following generic Property classes:

• gov.nasa.jpf.jvm.NotDeadlockedProperty - for every non-end state, test if there is any runnable threadleft
• gov.nasa.jpf.jvm.NoAssertionViolatedProperty - test if any assertion expression has been violated
• gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty - test if any exception was not handled inside the application

New properties can be added by providing additional implementors of the gov.nasa.jpf.Property interface

public interface Property extends Printable {
  boolean check (Search search, VM vm);
  String getErrorMessage();
}

or, to save some efforts mostly associated with printing out error traces, by deriving classes from gov.nasa.jpf.GenericProperty, which requires only the check(..) method to be overriden. To configure these new checks, add them to the colon separated list of classnames specified under search.properties in a JPF configuration file (either default or mode specific):

search.properties=\
    gov.nasa.jpf.jvm.NotDeadlockedProperty:\
    gov.nasa.jpf.jvm.NoAssertionViolatedProperty:\
    gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty:\
    x.y.z.MyNewProperty

(3) gov.nasa.jpf.SearchListener and gov.nasa.jpf.VMListener instances can be used to implement more complex checks that do require more information than what is available after a transition got executed. The rich set of callbacks enables listeners to monitor almost all JPF operations and translate them into internal state. JPF execution control can be achieved in two ways:

• by implementing both the appropriate listener interface and the gov.nasa.jpf.Property interface, then registering with Search.addProperty(..), to let JPF automatically check for violated property termination between states.
• by calling Search.terminate() to stop searching for new states. This can be done from anywhere within the listener, but does not automatically create error reports, which have to be done explicitly by the listener.

To ease property creation, JPF includes a gov.nasa.jpf.PropertyListenerAdapter class, which can be used as base class for complex properties. Subclasses only have to implement the interface methods they are interested in, property registration is performed automatically during the SearchListener.searchStarted notification. The typical design for such a subclass is to use VMListener methods to determine when the property fails, and then store this condition in a field which is evaluated in the Property.check() method.

public class MyPropertyListener extends PropertyListenerAdapter {
  boolean propertyHolds = true;
  ..
  
  /********************** Property interface **************/
  public boolean check (Search search, VM vm) {
    return propertyHolds;
  }
  
  public String getErrorMessage () {    
    return "My property violated " + ...;
  }
  
  /********************** VMListener interface *************/
  public void instructionExecuted (VM vm) {
    JVM jvm = (JVM)vm;
    Instruction insn = jvm.getLastInstruction();
    
    if (insn instanceof ...) {
       .. propertyHolds = false; ..
    }
  }
}

Examples of complex properties following this scheme can be found in directory src/gov/nasa/jpf/tools (e.g. RaceDetector). Note that JPF might still execute instructions after the property failure was detected, since the check() method is only called after the transition is completed.

Registration is performed via the jpf.listener property, either via command line

> bin/jpf .. +jpf.listener=MyPropertyListener ..

or the mode property file (e.g. jpf.properties)

..jpf.listener = ..:MyListener:..