Integrating software testing and run-time checking in an assertion verification framework

Mera, E. and López García, Pedro and Hermenegildo, Manuel V. (2009). Integrating software testing and run-time checking in an assertion verification framework. In: "25th International Conference on Logic Programming", July 14-17, 2009, Pasadena, CA, USA. ISBN 978-3-642-02845-8.

Description

Title: Integrating software testing and run-time checking in an assertion verification framework
Author/s:
  • Mera, E.
  • López García, Pedro
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: 25th International Conference on Logic Programming
Event Dates: July 14-17, 2009
Event Location: Pasadena, CA, USA
Title of Book: ICLP '09 Proceedings of the 25th International Conference on Logic Programming
Date: 2009
ISBN: 978-3-642-02845-8
Volume: 5649
Subjects:
Freetext Keywords: Dynamic verification, Unit testing, Static/dynamic debugging, Assertions, Verificación dinámica, Pruebas unitarias, Depuración estática y dinámica, Aseveraciones.
Faculty: Facultad de Informática (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview

Abstract

We have designed and implemented a framework that unifies unit testing and run-time verification (as well as static verification and static debugging). A key contribution of our approach is that a unified assertion language is used for all of these tasks. We first propose methods for compiling runtime checks for (parts of) assertions which cannot be verified at compile-time via program transformation. This transformation allows checking preconditions and postconditions, including conditional postconditions, properties at arbitrary program points, and certain computational properties. The implemented transformation includes several optimizations to reduce run-time overhead. We also propose a minimal addition to the assertion language which allows defining unit tests to be run in order to detect possible violations of the (partial) specifications expressed by the assertions. This language can express for example the input data for performing the unit tests or the number of times that the unit tests should be repeated. We have implemented the framework within the Ciao/CiaoPP system and effectively applied it to the verification of ISO-prolog compliance and to the detection of different types of bugs in the Ciao system source code. Several experimental results are presented that ¡Ilústrate different trade-offs among program size, running time, or levéis of verbosity of the messages shown to the user.

More information

Item ID: 14304
DC Identifier: http://oa.upm.es/14304/
OAI Identifier: oai:oa.upm.es:14304
Official URL: http://link.springer.com/chapter/10.1007%2F978-3-642-02846-5_25
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 18 Jan 2013 08:06
Last Modified: 21 Apr 2016 13:54
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM