Extensibility

From the list of JPF features mentioned above, it should be clear that the system is not a classical model checker anymore. One can think of JPF as an execution system framework for all kinds of dynamic, runtime oriented verification purposes. JPF tries to overcome the systematic scalability problem of software model checking by application- and property- specific adaptation. As a consequence, the major design force driving it's further development is extensibility. This document includes descriptions of four major extension mechanisms:

  1. Search-/VMListeners
  2. Model Java Interface (MJI)
  3. Configurable ChoiceGenerators
  4. Bytecode Factories

(1) Search- /VMListeners provide a convenient way to extend JPFs internal state model, add more complex property checks, direct searches, or simply gather execution statistics. This is achieved by an Observer pattern that lets concrete observers (listeners) subscribe to certain events inside JPF, like bytecode instruction execution or forward/backtrack steps.

(2) The Model Java Interface (MJI) is a mechanism to separate and communicate between state-tracked execution inside the JPF JVM, and non-state tracked execution inside the underlying host VM (executing JPF itself). This can be used to build standard library abstractions that significantly reduce the application state space.

(3) Configurable ChoiceGenerators (CGs) are used to implement application specific heuristics for "non-deterministic" data acquisition and scheduling policies, without the need to modify test drivers. ChoiceGenerators can be specified and parameterized via the normal JPF configuration mechanism, and used from within MJI native methods and Listeners.

(4) Bytecode Factories are the measure of choice if you want to change the execution mode. There are classes that represent every bytecode type, which normally get instatiated from the instruction objects we get from BCEL, which in turn loads the class files. Main responsibility of these Instruction objects is to provide an execute() method that represents the behavior of instructions. The BytecodeFactory interface provides the capability to overload any number of these classes, to change JPF's execution mode. Most prominent application of this infrastructure is the symbolic execution extension, which uses it to generate concrete test cases.