Laboratoire d'Informatique de
l'université de Franche-Comté
CNRS FRE 2661

JML-Testing-Tools: JML specification animator

The JML animator is a simple and direct way to simulate the execution of a JML specification. It makes it possible to constrain the input parameters of the executed methods, and to valuate the constrained states therefore created. It is also possible to perform on-the-fly checking of properties such as class invariant or history constraints.
It relies on technologies created inside the BZ-Testing-Tools project.

This project has been realised within the Techniques Formelles et à Contraintes (Formal and Constrained Techniques) team, in the framework of the GECCOO (Génération de Code Certifié pour les applications Orientées Objet / Generation of Certified Code for Object-Oriented applications) and CASSIS (Combinaison d'Approches pour la Sécurité des Systèmes InfiniS / Combining Approaches for the Satefy of Infinites Systems) projects.

To get the JML animator, you have to register. Registration is free.

JML-Testing-Tools: what is it?

JML-Testing-Tools is a tool-set for the validation of a formal specification written in JML using symbolic animation and automated boundary black-box test generation for Java.

This approach is based on the symbolic animation of the JML specification. This allows a user to validate its specification for the model-based test generation. Symbolic animation uses constraint solvers to manage the system state variables values.
The use of constraints make it possible for the user to leave the method parameters unspecified during the animation. These parameters are said to be "constrained", which means that they are assigned to a symbolic value which satisfies the methods pre- and postconditions to guarantee the method execution.

The architecture of JML-Testing-Tools is given below.

The Java/JML file is analysed and translated into an intermediate format file, name BZPE. The symbolic animation et the test generation processes rely on this format.

The mechanism of symbolic animtion of JML specifications

The animation of the specification uses the JML method specifications to simulate their executions, without taking the Java code into account. Thus, the method execution is based on the pre- and postconditions expressed in first order logic. This makes it possible, from a before state, to compute the after state. Animating a JML specification consists in solving a constraint satisfaction problem between the state before Be(X) (with a vector X of state variables), the state after Af(X,X') (with a vector X' of state variables after) and the constraints obtained from the behaviors of the method specifications M(X,X'). The consistency of Av(V) && M(X,X') && Ap(V,V') ensures the activability of the method M.

The animation interface is displayed hereafter.

We can see on this screenshot :

The system state in the left area, which displays the created objects and their attributes' values.
The Java execution sequence in the top-left area.
The local variables, in the middle-right area, added by the user, classified between object-typed variables and built-in types variables.
The property checking information in the bottom-right area. During the execution, the animator makes it possible to check model properties such as invariants, and history constraints, and to exhibit counter-examples.

Test generation from JML specifications

Test generation relies on the symbolic representation of object states set up for the animation of the JML specifications. This representation makes it possible to compute boundary values for input parameters in order to generate test data. The target of the test generation is the activation of the behaviors that we extract from the JML method specifications. Therefore, the user chooses which methods he wants to activate ; they will define the test targets.

Specification coverage
The specification is covered through the activation of the behaviiors of the JML method specifications. In addition, we consider different rewritings for the disjunctions within the predicates defining the considered behavior. These rewritings satisfy different coverage criteria such as statement coverage, condition coverage, decision coverage, full predicate coverage, multiple condition coverage.

Data coverage
Data coverage consists in selecting the boundary values for the method parameters. A boundary method parameter is either:

an object. In this case, its boundary values are considered as special object values such as null, this, an instance of the expected class, an instance of one of its subclasses, or the same value as another parameter. The impossible configurations are obviously detected and filtered at test generation-time.
a numerical value. In this case, the boundary values are taken at the bounds of the numerical value domain, reduced by the constraints from the considered behavior.

The following screenshot illustrates the choice of the specification and data coverage criteria.

Preamble computation and reification
A preamble computation is performed to automatically find an execution sequence (including object creations and method invokations) to reach a system state satisfying the activation of the considered behavior.
Finally, the test cases are translated into Java test sequences that can be directly executed on the Java program.

The test generator is not yet available for download.

Questions, comments, suggests? Write to jmltt@lifc.univ-fcomte.fr