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

Mera, E.; López García, Pedro y Hermenegildo, Manuel V. (2009). Integrating software testing and run-time checking in an assertion verification framework.. Monografía (Informe Técnico). Facultad de Informática (UPM) [antigua denominación], Madrid, Spain.

Descripción

Título: Integrating software testing and run-time checking in an assertion verification framework.
Autor/es:
  • Mera, E.
  • López García, Pedro
  • Hermenegildo, Manuel V.
Tipo de Documento: Monográfico (Informes, Documentos de trabajo, etc.) (Informe Técnico)
Fecha: Marzo 2009
Materias:
Palabras Clave Informales: dynamic verification, unit testing, static/dynamic debugging, assertions, verificación dinámica, pruebas de unidad, depuración estática/dinámica, afirmaciones.
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (1MB) | Vista Previa

Resumen

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.

Más información

ID de Registro: 15369
Identificador DC: http://oa.upm.es/15369/
Identificador OAI: oai:oa.upm.es:15369
URL Oficial: http://clip.dia.fi.upm.es/~herme/engcurnew/engcurnew.html
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 18 May 2013 06:55
Ultima Modificación: 21 Abr 2016 15:25
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM