Generación de casos de prueba tipo caja negra mediante restricciones

Abstract

La plataforma de validación CAVI-ART nos ofrece una representación intermedia de cualquier función escrita en diferentes lenguajes de programación, que incluye su código, su precondición y su postcondición. Sobre dicha función deseamos realizar pruebas de ejecución. El objetivo de este trabajo reside en crear de manera automática diferentes casos de prueba que cumplan las precondiciones de las funciones que se quieran probar. Para ello, se han estudiado primero los resolutores SMT, en concreto Z3, se han programado en tal resolutor todas las funciones y tipos que pueden interesarnos para las precondiciones, y por último se ha creado, en Haskell, un generador de restricciones que analice las precondiciones de un programa en la IR, gracias a su representación en forma de árbol abstracto, y genere un archivo de restricciones procesable por Z3 con el que obtener los casos de prueba.

The validation platform CAVI-ART offers us an intermediate representation for any function written in different languages, including its precondition, its code and its postcondition. We want to do testing of those functions. The goal of this work consists of automatically creating different test cases satisfying the preconditions of the functions wanted to be tested. In order to do this, SMT solvers have been studied, specifically Z3, every function and datatype we could be interested in for the preconditions have been programmed, and, finally, a constraints generator has been created in Haskell. It analyzes the preconditions of an IR program, thanks to its abstract syntax tree representation, and generates a constraints file processable by Z3 from which we obtain the test cases.