A methodology for applying concolic testing

Cherep Dragoevich, Manuel (2016). A methodology for applying concolic testing. Proyecto Fin de Carrera / Trabajo Fin de Grado, E.T.S. de Ingenieros Informáticos (UPM), Upsala, Suecia.

Description

Title: A methodology for applying concolic testing
Author/s:
  • Cherep Dragoevich, Manuel
Contributor/s:
  • Sagonas, Konstantinos
  • Pearson, Justin
  • Gällmo, Olle
Item Type: Final Project
Degree: Grado en Matemáticas e Informática
Date: September 2016
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Otro
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 (241kB) | Preview

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.

More information

Item ID: 54971
DC Identifier: http://oa.upm.es/54971/
OAI Identifier: oai:oa.upm.es:54971
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 16 May 2019 09:55
Last Modified: 16 May 2019 09:55
  • 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