QUEST

QUEST is a suite of tools integrated in a Eclipse plug-in that aim to ensure compliance of  Java implementations of data abstractions with their property-driven specifications.

 

The general aim of QUEST suite of tools is to ensure the compliance of Java implementations of abstract data types (ADT) with their specifications. Specifications are property-driven, can be parameterized (by other specifications), and support the specification of ADTs independently of the programming language and programming paradigm.

The suite of tools, integrated in an Eclipse plug-in, is composed of:

  • 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.

QUEST Eclipse plug-in supports the writing of ADT specifications, the run-time verification of implementations against specifications, the automatic localisation of faults and the generation of test suites.

 

QUEST diagram 

Team

Antónia Lopes
Vasco T. Vasconcelos
Isabel Nunes
João Pascoal Faria (FEUP)
Jorge Delgadillo Branco
Rui Gameiro
Ana Costa Santos
Filipe Luís
Francisco Andrade (FEUP)
Francisco Silva (FEUP)

Project

QUEST: A Quest for Reliability in Generic Software Components

Downloads

Eclipse QUEST plugin
Update Site

http://www.di.fc.ul.pt/~mal/QUEST/updateSite

Requirements
Installing the Eclipse QUEST Plugin
      • In Eclipse go to the Help Menu → Install New Software…
      • Copy the update site link http://www.di.fc.ul.pt/~mal/QUEST/updateSite to the work withfield and press Enter.
      • Select QUEST and unselect the “Contact all update sites during install to find the required software” option (the last in the screen).
      • Press the Next button and follow the installation instructions. Also, trust us and accept the unsigned plugin.
      • Restart Eclipse. The installation is now complete

Important Information:

    • Locate the Eclipse directory on a directory path with no spaces.
    • The plug-in does not work with more recent versions of Eclipse (eg., Luna or Mars).
    • The plug-in makes use of the console javac command, so make sure you have it available (use the command java -version to get the version).
    • The build path of your ConGu projects should include the JRE for that same version of Java.
    • Eclipse should be running with the same version of Java. Hence, users with Mac OS running Java 7 or later, if asked to install Java 6 to run Eclipse Juno or Kepler, should start Eclipse application with the command line.

Quick Tutorial

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
  1. 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 in the examples section. The project includes a specification of a sorted set and an implementation of this ADT defined in terms of a tree.

2. 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

3. 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.

4. 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

Publications

F.Rebelo de Andrade, J.P.Faria, A.Lopes e A.C.R.Paiva , Specification-driven unit test generation for Java Generic Classes, D.Latella and H. Treharne , Integrated Formal Methods, LNCS 7321, pp. 296-311 , Springer-Verlag Berlin Heidelberg , 2012 ifm2012.pdf

I.Nunes e F.Luís , A fault-location technique for Java implementations of algebraic specifications, DI-FCUL-TR-2012-02 , February 2012   TR-2012-02.pdf

Filipe Miguel Martins Serra Luís, Msc Thesis Engenharia Informática, FCUL, Refinamento de teste para localização de faltas, September  2012

Francisco Ricardo Pinto da Silva, Msc Thesis Engenharia Informática e Computação, FEUP, Geração Automática de Testes a partir de Especificações Algébricas, June  2012

F.Luís e I.Nunes , Congu/Flasji: Uma ferramenta para localização de faltas em implementações Java de especificações algébricas, INFORUM – Simpósio de Informática (poster session), Univ. Nova de Lisboa, Portugal , 6-7 September, 2012

A.Garis, A.C.R.Paiva, A.Cunha, D.Riesco , Specifying UML protocol state machines in Alloy, D.Latella and H. Treharne , Integrated Formal Methods, LNCS 7321, pp. 322-326 , Springer-Verlag Berlin Heidelberg , 2012

P.Crispim, A.Lopes and V.Vasconcelos, Runtime Verification for Generic Classes with ConGu 2 , in J. Davies, L. Silva, and A. Simão (Eds.): Formal Methods: Foundations and Applications, Revised Selected Papers, 13th Brazilian Symposium on Formal Methods , Springer-Verlag Berlin Heidelberg (2011) , SBFM 2010, Natal, Brasil, Nov. 2010, LNCS 6527, pp. 33–48, 2010 ConGu2.pdf

Francisco Xavier Richardson Rebello de Andrade, Msc Thesis Engenharia Informática e Computação, FEUP, Automatic Generation of Test Cases derived from Algebraic Specifications, June , 2010

P.Crispim, A.Lopes e V.Vasconcelos , Monitorização da Correcção de Classes Genéricas, Actas do 2º Encontro Nacional de Informática, INFORUM 2010, Braga, Portugal, Setembro de 2010, TR, Universidade do Minho. Best Student Paper Award, 2010

I.Nunes, A.Lopes and V.Vasconcelos, Bridging the Gap between Specification and Object-oriented Generic Programming, Runtime Verification, 9th International Workshop — Selected Papers, LNCS 5779, pp. 115-131 , Springer , 2009  rv 2009.pdf

F.Rebelo de Andrade, J.P.Faria, A.Lopes e A.C.R.Paiva , Specification-driven unit test generation for Java Generic Classes, TR-QUEST-2011-01, FEUP , 2011  TR-QUEST-2011-01.pdf

F.Rebelo de Andrade, J.P.Faria, A.C.R.Paiva e A.Lopes , Geração de Testes a partir de Especificações Algébricas de Tipos Genéricos usando Alloy , Actas do 3º Encontro Nacional de Informática, INFORUM 2011, Coimbra, Portugal, Setembro de 2011, TR, Universidade de Coimbra (2011) , 2011  INFORUM2011.pdf

F.Rebelo de Andrade, J.P.Faria and A.C.R.Paiva , Test Generation from Bounded Algebraic Specfications Using Alloy , SciTePress 2011, Seville, Spain , 18-21 July , ICSOFT- Proceedings of the 6th International Conference on Software and Data Technologies, pp. 192-200 , 2011 ICSOFT2011.pdf 

I.Nunes e F.Luís , Testing Java implementations of algebraic specifications, In Alexander K. Petrenko and Holger Schlingloff: Proceedings Eighth Workshop on Model-Based Testing (MBT 2013) , Rome, Italy, 17th March 2013, Electronic Proceedings in Theoretical Computer Science 111, pp. 35–50, 2013 ArXived at DOI:10.4204/EPTCS.111.4

I. Nunes and F. Luís , A 5-step hunt for faults in Java implementations of algebraic specifications, Proceedings of 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2013). ISBN 978-0-7695-4993-4 , 2013

Examples

Below you can find some examples, ready to be used in QUEST Plug-in.
Each example includes a specification module describing an ADT (one or more specification files and possibly a module file), a Java implementation of the ADT (and possibly some classes used for instantiating the parameters) and a refinement mapping.

Non-generic ADTs:

Parameterized ADTs without constraints over parameters:

Parameterized ADTs with constraints over parameters: