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. En: "25th International Conference on Logic Programming", July 14-17, 2009, Pasadena, CA, USA. ISBN 978-3-642-02845-8.

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: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: 25th International Conference on Logic Programming
Fechas del Evento: July 14-17, 2009
Lugar del Evento: Pasadena, CA, USA
Título del Libro: ICLP '09 Proceedings of the 25th International Conference on Logic Programming
Fecha: 2009
ISBN: 978-3-642-02845-8
Volumen: 5649
Materias:
Palabras Clave Informales: Dynamic verification, Unit testing, Static/dynamic debugging, Assertions, Verificación dinámica, Pruebas unitarias, Depuración estática y dinámica, Aseveraciones.
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 ¡Ilústrate different trade-offs among program size, running time, or levéis of verbosity of the messages shown to the user.

Más información

ID de Registro: 14304
Identificador DC: http://oa.upm.es/14304/
Identificador OAI: oai:oa.upm.es:14304
URL Oficial: http://link.springer.com/chapter/10.1007%2F978-3-642-02846-5_25
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 18 Ene 2013 08:06
Ultima Modificación: 21 Abr 2016 13:54
  • 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