Abstract
Las pruebas de software, conocidas como “testing”, son el método predominante en la industria para asegurar que un programa es correcto y fiable. Como resultado de la creciente complejidad del software existen errores cada vez más difíciles de encontrar, lo que requiere técnicas de “testing” más sofisticadas. Para mejorar la cobertura y fiabilidad del software se han desarrollado herramientas y técnicas de “testing” automático. Algunas de estas técnicas usan “testing” aleatorio donde los valores de entrada de los programas se generan aleatoriamente. El problema que tienen dichas técnicas es que diferentes valores de entrada pueden estar “testeando” repetidamente un mismo comportamiento del código. Esto significa que valores de entrada aleatorios no garantizan la cobertura de diferentes ramas de ejecución. Además, estas técnicas requieren que se escriban manualmente propiedades de los programas que van a ser “testeados”. “Concolic testing” es una técnica que combina la ejecución concreta y simbólica de un programa. El objetivo es generar valores de entrada que ejercitan diferentes ramas de ejecución. Un programa se ejecuta de forma concreta y al mismo tiempo se recogen restricciones simbólicas durante la ejecución que forman un camino de restricción. Las restricciones en dicho camino se niegan y se resuelven sistemáticamente usando un demostrador de teoremas, generando así nuevos valores de entrada que ejercitan una rama de ejecución diferente. “Concolic testing” ha ganado popularidad en los lenguajes de programación imperativos como C y Java, sin embargo su uso en lenguajes de programación funcional es más reciente. CutEr, una herramienta que aplica “concolic testing” en Erlang es la primera herramienta que aplica dicha técnica en un lenguaje de programación funcional. Las herramientas de “concolic testing” son completamente automáticas y los valores de entrada de los programas se generan utilizando información de tipos disponible. Sin embargo, la mayoría de los lenguajes de especificación de tipos no son lo suficientemente expresivos. Si esto sucede, una herramienta de “concolic testing” puede generar valores que no respetan completamente el tipo esperado para después mostrarlos como valores que provocan errores en tiempo de ejecución. En este trabajo se propone una metodología universal, la primera en “concolic testing”, que garantiza el uso de valores de entrada bien formados y que ayuda a encontrar errores en la lógica de los programas.---ABSTRACT---Concolic testing is a technique that combines concrete and symbolic execution in order to generate inputs that explore different execution paths leading to better testing coverage. Concolic testing tools can find runtime errors fully automatically using available type specifications. The type specifications in a function define the type of each input. However, most specification languages are never expressive enough, which can lead to runtime errors caused by malformed inputs (i.e. irrelevant errors). Moreover, logic errors causing a program to operate incorrectly without crashing cannot be reported automatically. A universal methodology for any programming language is proposed. Preconditions force the concolic execution to generate well formed inputs before testing a function. On the other hand, postconditions lead to a runtime error when a program operates incorrectly, helping to find logic errors. The results obtained using the concolic testing tool CutEr, in the functional programming language Erlang, show how a program is only tested using well formed inputs specially generated to try to violate the defined postconditions.
