Property Specifications: The most straightforward way to specify and check simple safety properties in JPF is to use Java assertions inside the application under analysis. This allows the specification of properties that only depend on the application data values (e.g., parameter value intervals). Violations are caught by JPF. The drawbacks of this method are that it requires access to the 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).
The other way to specify properties is by using gov.nasa.jpf.Property or gov.nasa.jpf.GenericProperty instances to encapsulate property checks.
The user typically creates an instance of such a class and provides an implementation for its check() method which does the main work for checking the property. The check()method is evaluated after each transition. If it returns false and termination has been requested, the search process ends, and all violated properties are printed (which potentially includes error traces).
JPF comes with generic Property classes for the following properties:
- No Deadlocks
- No Assertion Violation
- No Uncaught Exceptions (i.e., not handled inside the application)