eprintid: 15369
rev_number: 19
eprint_status: archive
userid: 2047
dir: disk0/00/01/53/69
datestamp: 2013-05-18 06:55:23
lastmod: 2023-02-27 08:21:33
status_changed: 2023-02-27 08:21:33
type: monograph
metadata_visibility: show
item_issues_count: 0
creators_name: Mera, E.
creators_name: López García, Pedro
creators_name: Hermenegildo, Manuel V.
title: Integrating software testing and run-time checking in an assertion verification framework.
ispublished: pub
subjects: informatica
keywords: dynamic verification, unit testing, static/dynamic debugging, assertions, verificación dinámica, pruebas de unidad, depuración estática/dinámica, afirmaciones.
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.
date: 2009-03
date_type: published
publisher: Technical University of Madrid (UPM)
official_url: http://clip.dia.fi.upm.es/~herme/engcurnew/engcurnew.html
full_text_status: public
monograph_type: technical_report
place_of_pub: Madrid, Spain
pages: 19
institution: Informatica
department: Inteligencia_Artificial
refereed: TRUE
rights: by-nc-nd
citation:   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) <https://oa.upm.es/view/institution/Informatica/>, Madrid, Spain.    
document_url: https://oa.upm.es/15369/1/HERME_TCREP_ANDMANS_2009-6.pdf