An integrated approach to assertion-based random testing in logic languages

Casso San Román, Ignacio (2021). An integrated approach to assertion-based random testing in logic languages. Thesis (Master thesis), E.T.S. de Ingenieros Informáticos (UPM).

Description

Title: An integrated approach to assertion-based random testing in logic languages
Author/s:
  • Casso San Román, Ignacio
Contributor/s:
  • Hermenegildo Salinas, Manuel Vicente
Item Type: Thesis (Master thesis)
Masters title: Inteligencia Artificial
Date: July 2021
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (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 (265kB) | Preview

Abstract

En este trabajo presentamos un método para testear programas en Prolog, integrado en un modelo de desarrollo basado en aserciones. Nuestro punto de partida es el lenguaje Ciao y su modelo de aserciones, que unifica la verificación y comprobación de errores dinámica y estática, usando un lenguaje de aserciones común. En este modelo, cuando alguna propiedad no se puede verificar estáticamente, se instrumenta el código fuente para que la propiedad se compruebe dinámicamente en tiempo de ejecución, y en particular en la fase de tests unitarios, si se han especificado tests con valores de entrada concretos. En este contexto, la idea de generar automáticamente entradas aleatorias para los tests unitarios a partir de las precondiciones de las aserciones surge de manera natural, dado que estas precondiciones son conjunciones de literales, y sus predicados correspondientes se pueden usar en principio como generadores. En este trabajo desarrollamos LPtest, una herramienta que implementa la idea anterior, generando automáticamente entradas relevantes para testear una amplia variedad de propiedades de los predicados de un programa. El algoritmo de generación está basado en ejecutar los predicados usando reglas de búsqueda aleatorias. Se proponen también métodos para soportar propiedades específicas de programación lógica, incluyendo combinaciones de tipos y compartición e instanciación de variables, así como ideas para reducir los casos de prueba y para mejorar la generación aprovechando la información inferida por el análisis estático. Como caso de estudio de la herramienta, se aplica LPtest al testeo del analizador estático basado en interpretación abstracta de Ciao. Se proponen dos métodos diferentes para abordar el problema usando testeo aleatorio basado en aserciones. En el primero, se especifican mediante aserciones de Ciao algunas propiedades teóricas básicas que deben cumplir los dominios abstractos y sus operaciones para ser correctos. Después se aplica la herramienta sobre esas aserciones para validar el código de algunos dominios abstractos en Ciao. El segundo método consiste en comprobar, para un conjunto de programas de prueba, que las aserciones que infiere estáticamente el analizador se satisfacen dinámicamente, usando para ello LPtest. Esta idea se puede implementar y automatizar fácilmente aprovechando el sistema de aserciones integrado de Ciao y sus componentes: el analizador estático, que expresa sus resultados mediante un nuevo programa idéntico al original pero con aserciones intercaladas; y LPtest, que genera y ejecuta casos de prueba que satisfacen las propiedades que aparecen en las precondiciones de dichas aserciones. Los dos métodos se implementan y se aplican para testear CiaoPP y sus dominios abstractos, encontrando en el proceso errores no triviales y desconocidos anteriormente.---ABSTRACT---We present an approach for assertion-based random testing of Prolog programs that is tightly integrated within an overall assertion-based program development scheme. Our starting point is the Ciao model, a framework that unifies unit testing and runtime verification, as well as static verification and static debugging, using a common assertion language. Properties which cannot be verified statically are checked dynamically. In this context, the idea of generating random test values from assertion preconditions emerges naturally since these preconditions are conjunctions of literals, and the corresponding predicates can in principle be used as generators. We develop LPtest, a tool that generates valid inputs from the properties that appear in the assertions shared with other parts of the model, and uses the run time-check instrumentation of the Ciao framework to perform a wide variety of checks. The generation process is based on running standard predicates under non-standard (random) search rules. We propose methods for supporting (C)LP-specific properties, including combinations of shape-based (regular) types and variable sharing and instantiation, and we also provide some ideas for shrinking for these properties and for enhancing generation by exploiting information inferred by the analyzer. As a case study, we apply LPtest for testing Ciao’s abstract interpretation-based static analyzer. We approach this problem, using assertion-based random testing, in two different ways. In the first one, we encode into Ciao assertions some basic theoretical properties that abstract domains must satisfy in order to be sound. Then we apply the tool to those assertions to check and validate the code of some the abstract domains in the Ciao system. The second method consists in checking, over a suite of benchmarks, that the assertions inferred statically by the analyzer are satisfied dynamically, testing them with LPtest. This can be implemented and automatized with little effort by framing it within the Ciao integrated assertion framework and combining its components: the static analyzer, which outputs its results as the original program source with assertions interspersed; and the newly developed random testing framework, which generates and executes random test cases satisfying the properties present in assertion preconditions, relying on the run-time checking instrumentation and the unit-test framework. We apply both approaches to test some of CiaoPP’s analysis domains, successfully finding non-trivial, previously undetected bugs.

More information

Item ID: 68748
DC Identifier: https://oa.upm.es/68748/
OAI Identifier: oai:oa.upm.es:68748
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 08 Oct 2021 13:50
Last Modified: 08 Oct 2021 13:50
  • 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