QUEST: A Quest for Reliability in Generic Software Components

This is the site of QUEST, a project funded by FCT (PTDC/EIA-EIA/103103/2008).

QUEST: Executive Summary

The importance of data abstractions (DAs) in computing has long been recognised. The use of structurally complex data is prevalent in computer programs and modern software is no exception: for example, web-traversal programs operate on graphs that encode web pages, and IDEs manipulate abstract syntax trees corresponding to program representations.

Developers can either program their own implementations of the required DAs, or use components off-the-shelf (COTS) available in a myriad of libraries and frameworks. However, we have been assisting to an increasing tendency to rely on code reuse, most of it produced by open consortiums, without any sort of certification. In both cases, it is important that developers, possibly assisted by practical tools, can easily gain confidence about the reliability of the produced/reused code. It is our understanding that this vision requires that developers have available, integrated in their development environments:

  1. practical notations to formally specify DAs, and
  2. effective techniques, simple to use and non time consuming, that allow to gain confidence that a given set of components correctly implements the specified DAs.

This is the general problem we propose to address in the context of QUEST.

The described problem has been addressed by several researchers in different ways but, as solutions available are not fully satisfactory, it continues to attract attention. Recent publications in top conferences and journals demonstrate our point. QUEST’s innovative aspects are mainly related with the nature of the components that will be addressed — generic components, i.e., components that, through instantiation, can be used in different scenarios. Our focus will be on components programmed in Java, one of today´s most popular programming languages (actually ranking first at TIOBE Index), but we seek techniques that can be applied to other modern OO languages. We are especially interested in addressing generic components because, although Java generic implementations of DAs became common since generic types were introduced in the language, available analysis solutions are not applicable to them. Other key concern is that the developed techniques have to be applicable to components in a black-box manner so that their reliability can be assessed even if executable code and documentation is all that is available (as often happens with COTS). Finally, we also plan to contribute with techniques that in the presence of a failure help to interpret it and to locate the errors in the code that may have caused it.

The aim is to contribute with an approach to the problem considering that:

  1. DAs are specified in terms of property-driven specifications, independent of the programming language used for development;
  2. correctness of a component is analysed through runtime checking the specified properties;
  3. effectiveness of the process, while keeping it completely automated, requires the automatic generation and execution of effective test suites; test generation can be guided by the specification, also taking into account the specificity of the target.

The main results of the project will be the development and integration of different techniques resulting into a push-button approach to reliability analysis of Java implementations of DAs. These techniques will be made available in the form of tools integrated in a popular Java IDE.

The results achieved will be disseminated via the usual channels — TRs, MsC/PhD thesis, papers and talks. The produced tools will be made available in the project web site together with the case studies carried out in the project. Furthermore, the results and tools will be used for teaching in graduate and postgraduate courses in Informatics in the two involved universities. The research team gathered to the quest for these goals comprises elements from two sites, with complementary research expertise that covers the lines of research involved in QUEST.

QUEST: Team


PhDs

Students

Past Members

QUEST: Publications

Locating Faults in Java Implementations of Algebraic Specifications

I.Nunes e F.Luís, June 2012, submitted

Specification-driven unit test generation for Java Generic Classes

F.Rebelo de Andrade, J.P.Faria, A.Lopes e A.C.R.Paiva, in D.Latella and H. Treharne (Eds..), Integrated Formal Methods, iFM 2012, Pisa, Italy, June 2012,LNCS 7321, pp. 296-311. Springer-Verlag Berlin Heidelberg (2012)

A fault-location technique for Java implementations of algebraic specifications

I.Nunes e F.Luís, DI-FCUL-TR-2012-02, DOI:10455/6809 , Departamento de Informática, FCUL (2012)

Specification-driven unit test generation for Java Generic Classes

F.Rebelo de Andrade, J.P.Faria, A.Lopes e A.C.R.Paiva, TR-QUEST-2011-01, FEUP (2011)

Geração de Testes a partir de Especificações Algébricas de Tipos Genéricos usando Alloy

F.Rebelo de Andrade, J.P.Faria, A.C.R.Paiva e A.Lopes, Actas do 3º Encontro Nacional de Informática, INFORUM 2011, Coimbra, Portugal, Setembro de 2011, TR, Universidade de Coimbra (2011)

Test Generation from Bounded Algebraic Specfications Using Alloy

F.Rebello de Andrade, J.P.Faria and A.C.R.Paiva, ICSOFT- Proceedings of the 6th International Conference on Software and Data Technologies, Volume 2, Seville, Spain, 18-21 July, 2011. SciTePress 2011, pp. 192-200 (2011)

Automatic Generation of Test Cases derived from Algebraic Specifications

Francisco Xavier Richardson Rebello de Andrade, Msc Thesis Engenharia Informática e Computação, FEUP, June de 2010, (supervision: João Pascoal Faria, co-supervision: Ana Cristina Paiva) (2010)

Runtime Verification for Generic Classes with ConGu2

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

Monitorização da Correcção de Classes Genéricas

P.Crispim, A.Lopes e V.Vasconcelos, Actas do 2º Encontro Nacional de Informática, INFORUM 2010, Braga, Portugal, Setembro de 2010, TR, Universidade do Minho. Best Student Paper Award

Bridging the Gap between Specification and Object-oriented Generic Programming

I.Nunes, A.Lopes and V.Vasconcelos, Runtime Verification, 9th International Workshop — Selected Papers, LNCS 5779, pp. 115-131, Springer, 2009

QUEST: Events

2ndYearMeeting (FCUL, from May 17, 2011 11:00 AM to May 17, 2011 03:30 PM)

Reunião de segundo do ano do projecto.


Kickoff meeting (FCUL, 6.3.05, from Mar 10, 2010 11:00 AM to Mar 10, 2010 03:00 PM)

QUEST Kickoff meeting