Fajita : generación automática de casos de test basada en verificación acotada

Mostrar todas las versiones(2)

La generación de casos de test es una de las metodologías más utilizadas para verificar la calidad de un sistema de software. Si bien resulta más económica que otros acercamientos como la verificación formal, los costos de una validación exhaustiva siguen siendo muy elevados, por lo que en la mayorí...

Descripción completa

Detalles Bibliográficos
Autor principal: Ciolek, Daniel Alfredo
Otros Autores: Frias, Marcelo Fabián
Formato: Tesis de grado publishedVersion
Lenguaje:Español
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2012
Materias:
TESTING
GENERACION AUTOMATICA DE CASOS DE TEST
VERIFICACION ACOTADA
SAT-SOLVING INCREMENTAL
TACO
DYNALLOY
ALLOY
AUTOMATIC TEST CASE GENERATION
BOUNDED VERIFICATION
INCREMEN- TAL SAT-SOLVING
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000513_Ciolek
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000513_Ciolek_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-seminario_nCOM000513_Ciolek_oai
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (UBA)
language Español
orig_language_str_mv spa
topic TESTING
GENERACION AUTOMATICA DE CASOS DE TEST
VERIFICACION ACOTADA
SAT-SOLVING INCREMENTAL
TACO
DYNALLOY
ALLOY
TESTING
AUTOMATIC TEST CASE GENERATION
BOUNDED VERIFICATION
INCREMEN- TAL SAT-SOLVING
TACO
DYNALLOY
ALLOY
spellingShingle TESTING
GENERACION AUTOMATICA DE CASOS DE TEST
VERIFICACION ACOTADA
SAT-SOLVING INCREMENTAL
TACO
DYNALLOY
ALLOY
TESTING
AUTOMATIC TEST CASE GENERATION
BOUNDED VERIFICATION
INCREMEN- TAL SAT-SOLVING
TACO
DYNALLOY
ALLOY
Ciolek, Daniel Alfredo
Fajita : generación automática de casos de test basada en verificación acotada
topic_facet TESTING
GENERACION AUTOMATICA DE CASOS DE TEST
VERIFICACION ACOTADA
SAT-SOLVING INCREMENTAL
TACO
DYNALLOY
ALLOY
TESTING
AUTOMATIC TEST CASE GENERATION
BOUNDED VERIFICATION
INCREMEN- TAL SAT-SOLVING
TACO
DYNALLOY
ALLOY
description La generación de casos de test es una de las metodologías más utilizadas para verificar la calidad de un sistema de software. Si bien resulta más económica que otros acercamientos como la verificación formal, los costos de una validación exhaustiva siguen siendo muy elevados, por lo que en la mayoría de los casos se hace un balance entre el costo de afrontar las potenciales fallas y el esfuerzo destinado a la validación. En esta tesis se presenta una técnica de generación automática de casos de test que puede ser utilizada para reducir los costos de la verificación del software. La técnica busca un conjunto minimal de casos de test que logre un alto índice de cobertura según un criterio dado. La metodología resulta flexible ya que admite la instrumentación de distintos criterios frecuentemente utilizados en la práctica. La técnica presentada se basa en efectuar una verificación acotada siguiendo una especificación formal de un programa. La verificación acotada se hace mediante la traducción del programa junto con su especificación a un modelo formal. Luego, el modelo es analizado utilizando un SAT-Solver para obtener una traza de ejecución válida, resultado que es traducido a un caso test. Como parte de este trabajo se construyó un prototipo experimental llamado Fajita. La herramienta fue evaluada mediante la comparación contra herramientas del estado del arte. Durante el trabajo se analizan las ventajas que introducen la utilización de SAT-Solving incremental junto con distintas tácticas para la reducción del espacio de búsqueda (predicados de rupturas de simetrías y exploración iterativa). Se proponen, también, mejoras en algunos de los criterios de selección de casos de test comúnmente utilizados.
author2 Frias, Marcelo Fabián
author_facet Frias, Marcelo Fabián
Ciolek, Daniel Alfredo
format Tesis de grado
Tesis de grado
publishedVersion
author Ciolek, Daniel Alfredo
author_sort Ciolek, Daniel Alfredo
title Fajita : generación automática de casos de test basada en verificación acotada
title_short Fajita : generación automática de casos de test basada en verificación acotada
title_full Fajita : generación automática de casos de test basada en verificación acotada
title_fullStr Fajita : generación automática de casos de test basada en verificación acotada
title_full_unstemmed Fajita : generación automática de casos de test basada en verificación acotada
title_sort fajita : generación automática de casos de test basada en verificación acotada
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2012
url https://hdl.handle.net/20.500.12110/seminario_nCOM000513_Ciolek
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000513_Ciolek_oai
work_keys_str_mv AT ciolekdanielalfredo fajitageneracionautomaticadecasosdetestbasadaenverificacionacotada
_version_ 1824952627741327360
spelling I28-R145-seminario_nCOM000513_Ciolek_oai2024-12-17 Frias, Marcelo Fabián Galeotti, Juan Pablo Ciolek, Daniel Alfredo 2012-03 La generación de casos de test es una de las metodologías más utilizadas para verificar la calidad de un sistema de software. Si bien resulta más económica que otros acercamientos como la verificación formal, los costos de una validación exhaustiva siguen siendo muy elevados, por lo que en la mayoría de los casos se hace un balance entre el costo de afrontar las potenciales fallas y el esfuerzo destinado a la validación. En esta tesis se presenta una técnica de generación automática de casos de test que puede ser utilizada para reducir los costos de la verificación del software. La técnica busca un conjunto minimal de casos de test que logre un alto índice de cobertura según un criterio dado. La metodología resulta flexible ya que admite la instrumentación de distintos criterios frecuentemente utilizados en la práctica. La técnica presentada se basa en efectuar una verificación acotada siguiendo una especificación formal de un programa. La verificación acotada se hace mediante la traducción del programa junto con su especificación a un modelo formal. Luego, el modelo es analizado utilizando un SAT-Solver para obtener una traza de ejecución válida, resultado que es traducido a un caso test. Como parte de este trabajo se construyó un prototipo experimental llamado Fajita. La herramienta fue evaluada mediante la comparación contra herramientas del estado del arte. Durante el trabajo se analizan las ventajas que introducen la utilización de SAT-Solving incremental junto con distintas tácticas para la reducción del espacio de búsqueda (predicados de rupturas de simetrías y exploración iterativa). Se proponen, también, mejoras en algunos de los criterios de selección de casos de test comúnmente utilizados. The generation of test cases is one of the most common software quality verification methodologies. While it tends to be more economical than other approaches such us formal verification, the costs of exhaustive validation still remain prohibitive; for that reason, most of the time a trade off between the costs of facing potential flaws and the effort destined to validation is made. In this thesis a technique for automatic test case generation is presented, which can be used to reduce the costs of software verification. The technique searches a minimal test set that achieves a high coverage index for a given test selection criterion. The methodology turns out to be flexible since it admits the instrumentation of different criteria frequently used in practice. The presented technique is based on making a bounded verification following a formal specification of a program. The bounded verification involves the translation of the program with its specification to a formal model. Then, the model is analyzed using a SAT-Solver in order to obtain a valid execution trace,which is finally translated to a test case. As part of this work, an experimental prototype called Fajita was built. The tool was evaluated by comparing it with state of the art tools. The advantages introduced by the usage of incremental SAT-Solving and different search space reduction tactics (symmetry breaking predicates and iterative exploration) are analyzed in this text. Also, improvements for some test selection criteria of wide usage are proposed. Fil: Ciolek, Daniel Alfredo. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000513_Ciolek spa Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar TESTING GENERACION AUTOMATICA DE CASOS DE TEST VERIFICACION ACOTADA SAT-SOLVING INCREMENTAL TACO DYNALLOY ALLOY TESTING AUTOMATIC TEST CASE GENERATION BOUNDED VERIFICATION INCREMEN- TAL SAT-SOLVING TACO DYNALLOY ALLOY Fajita : generación automática de casos de test basada en verificación acotada info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000513_Ciolek_oai

Ejemplares similares