Generación de casos de prueba de caja blanca mediante restricciones

Abstract

La plataforma CAVI-ART para la verificación automática de programas ofrece numerosas herramientas para el análisis de los mismos entre las que encontramos un generador de casos de prueba. El método seguido por el mismo se asemeja bastante a la fuerza bruta lo que desperdicia recursos y tiempo. El objetivo de este trabajo no es otro que mejorar sustancialmente el generador de casos de prueba. Se persigue conseguir un análisis de caja blanca guiado por el flujo de control del programa que permita generar casos certeros que comprueben hasta cierto punto todos los posibles caminos dentro del programa. Para ello analizaremos los programas según su naturaleza recursiva, desarrollaremos estrategias de análisis de los grafos de flujo de control para obtener caminos dentro de los mismos y traduciremos estos caminos a una serie de restricciones en el lenguaje SMT-LIB para finalmente obtener gracias al resolutor Z3 un modelo para las variables de entrada.The CAVI-ART platform for assisted program validation offers a set of tools for analyzing code among which we find a test-case generator. The actual method followed by this tool is quite similar to bruteforce and so, it wastes resources and time. The aim of this research is to substantially improve the test case generator. We want to achieve a whitebox analysis guided by the program’s control flow which will be used to generate accurate test cases that potentially check all the paths in a program. With this aim in mind, we will first analyze the recursive nature of the program, we will develop strategies for analyzing the control flow graphs in order to find paths through them and we will translate such paths into a sequence of constraints written in the SMT-LIB language in order to finally obtain, by means of the SMT solver Z3, a model for the input variables.