QUEST Tools Overview

QUEST Eclipse Plug-in

QUEST Eclipse Plug-in aggregates three tools that address the conformance checking of Java classes against specifications.

 

QUEST diagram

 

The underlying approach comprises

  • a language for defining property-driven algebraic specifications;
  • a language for defining refinement mappings between specifications and Java classes;
  • a conformance checking notion between algebraic specifications and Java classes;

and is supported by

  • ConGu, a tool that determines at run-time whether the classes that are subject to analysis behave as required by the specification;
  • GenT, a tool that automatically generates JUnit tests that check the conformance of a set of Java classes with respect to the specifications;
  • Flasji, a tool that automatically locates methods that are responsible for detected faults

ConGu

ConGu is a tool that determines at run-time whether the classes that are subject to analysis behave as required by the specification.

 

The tool performs the instrumentation of the bytecode of the classes under test, in order to intercept and forward certain method calls to automatically generated classes. Runtime checking of the specified properties at specific execution points is achieved directly by the generated code, relying on Java assertions.

 

During the execution of a system involving the classes under test, objects are checked against the specifications and the violations are reported. The correctness of clients' behaviour is also monitored whenever they use operations of the classes under test. In the case of generic classes with type constraints, it is also checked whether classes used to instantiate the parameters of generic classes conform to parameter specifications.

Run-time verification with ConGu

First of all, you have to create a ConGu project with

 

     File > New > Other > ConGu > ConGu Project

 

In addition to Java source code (in folder src), you need to provide the specifications and a refinement from these specifications to the Java classes (in folder spec).

It is also possible to import an existing ConGu project via

 

     File > Import > General > Existing Projects into Workspace

 

The screenshots presented in this page are based on the SortedSet ConGu project available here. The project includes a specification of a sorted set and an implementation of this ADT defined in terms of a tree.

 

Then, you should confirm that no syntactical errors exist via

 

     ConGu > Verify Refinement

 

Check refinement task

 

The presence of syntactical errors in the specifications or in the refinement is signaled in the respective files (see an example below).

 

Syntactical errors are marked in file

 

If your ConGu project has no syntactical errors, then the next step is to launch the ConGu compiler via

 

     ConGu > Compile for ConGu monitoring

 

The result of the compilation process is placed in the folder outputCongu.

 

In order to perform run-time verification, you need to have at least a Main class. You can create a run configuration for ConGu Monitoring as shown below. However, the easiest way is to use ConGu Monitoring shortcut. Simply select the root of the project in the package explorer view, right click, and navigate to

 

     Run As > ConGu Monitoring

 

Congu monitoring preferences

 

A violation of an axiom is reported in the form of a PostconditionException (see example below).

 

PostCondition Exception found

 

The invocation of a method that refines an operation in a situation in which th>e domain condition does not hold is reported in the form of a PreconditionException (see example below).

 

PreCondition exception found

 

ConGu may also check whether classes used to instantiate the parameters of generic classes conform to what was specified in the parameter specifications.

 

Congu refinement file

 

This requires to define a params file, explicitly indicating the classes that should be considered for each parameter (see example below).

GenT

GenT is a tool that automatically generates JUnit tests that check the conformance of a set of Java classes with respect to the specifications. The generated unit test cases for Java generic classes, in addition to the usual testing data, encompass implementation for the type parameters.

 

The proposed technique relies on the generation of several test goals for each axiom and the use of Alloy Analyzer to find model instances for each test goal. JUnit test cases and Java implementations of the parameters are extracted from these model instances.

Generating tests with GenT

In order to use GenT you also need to start creating a ConGu project with the Java source code (in folder src) and the specifications and a refinement between these specifications and the Java classes (in folder spec). Proceed as described before.

 

If your ConGu project has no syntactical errors, then the next step is to launch the GenT via

 

     ConGu > Launch GenT for creation of JUnit tests

 

The generated tests are placed in the folder outputTests. Right click on these folder and select

 

     Run As JUnit

 

Results obtained from GenT JUnit Test run

 

It is possible to define the number of elements of each sort that should be considered in the search for model instances. This search may take a while, depending, among other things, on the number of axioms. Progress is reported on the ConGu console in the form of the Alloy run commands that are being executed.

 

Through the properties of the ConGu project it is possible to configure some parameters that affect this search.

 

QUEST project properties page

Flasji

Flasji is a fault-location tool that points to methods whose behaviour is incorrect w.r.t. the specification. It compares actual to expected behaviour, that is, it compares the behaviour of “concrete” instances of the Java classes under test with the one they should have according to the specification. Flasji picks all behaviour deviations and interprets them, electing one or more methods as the one(s) that are most probably ill-implemented.

 

Since expected behaviour is given by the specifications, the method(s) Flasji points as guilty are among the ones that explicitly implement the specification operations as defined by the refinement mapping.

Locating Faults with Flasji

If ConGu or GenT found that the classes that are subject to analysis do not behave as required by the specifications, we can use Flasji to try to locate a method that contributes to the detected fault.

 

You can launch Flasji via

 

     ConGu > Launch Flasji for fault localization

 

The conclusions are reported in the ConGu console (see example below).

 

As with GenT above, the proposed technique relies on the use of the Alloy Analyzer to find model instances for the specification module. The concrete objects that are inspected for their behaviour are created according to these model instances. As before, it is possible to define both the number of elements that should be considered in the search for model instances and other parameters that affect the search.

 

Flasji fault location output results