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.. Monografía (Technical Report). Facultad de Informática (UPM), Madrid, Spain.

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: Monograph (Technical Report)
Date: March 2009
Subjects:
Freetext Keywords: dynamic verification, unit testing, static/dynamic debugging, assertions, verificación dinámica, pruebas de unidad, depuración estática/dinámica, afirmaciones.
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 illustrate different trade-offs among program size, running time, or levels of verbosity of the messages shown to the user.

More information

Item ID: 15369
DC Identifier: http://oa.upm.es/15369/
OAI Identifier: oai:oa.upm.es:15369
Official URL: http://clip.dia.fi.upm.es/~herme/engcurnew/engcurnew.html
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 18 May 2013 06:55
Last Modified: 21 Apr 2016 15:25
  • 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