Catálogo de publicaciones - tesis
Título de Acceso Abierto
Técnicas distribuídas para verificación acotada eficiente
Nicolás Leandro Rosner Marcelo Fabián Frias
publishedVersion.
Resumen/Descripción – provisto por el repositorio digital
El análisis formal de artefactos de software suele dividirse en dos clases de enfoques: pesados y livianos. Los métodos pesados ofrecen plena certeza del resultado obtenido pero requieren usuarios expertos. Los métodos livianos son más fáciles de aprender y se materializan en herramientas totalmente automáticas, pero la validez de sus resultados es parcial. Por ejemplo, en las técnicas de verificación exhaustiva acotada, la validez del resultado devuelto por la herramienta automática siempre está limitada por alguna noción de alcance o tamaño máximo configurable por el usuario. Para incrementar el grado de confianza en el resultado, el usuario sólo debe aumentar ese alcance y volver a ejecutar la herramienta. Sin embargo, el costo computacional del análisis automático es casi siempre exponencial en dicho alcance. En esta tesis presentamos una serie de técnicas y herramientas cuyo objetivo es mejorar la escalabilidad del análisis exhaustivo acotado de artefactos de software. En particular, nos interesa poder aprovechar la disponibilidad de hardware de bajo costo (como por ejemplo clusters de PCs, existentes en muchas empresas e instituciones) para extender la frontera de lo tratable mediante esta clase de enfoques. Por una parte presentamos transcoping, un enfoque incremental para explorar problemas de verificación exhaustiva acotada en tamaños pequeños y extrapolar la información recolectada para asistir la toma automática de decisiones en tamaños mayores del mismo problema. Mostramos su aplicación al análisis distribuido de modelos Alloy, así como a la toma de decisiones en la generación de casos de test basada en invariantes híbridos. También presentamos Ranger, otra técnica distinta para distribuir el análisis de modelos Alloy, que divide el problema en subproblemas de menor complejidad linealizando el espacio de potenciales contraejemplos y partiéndolo en intervalos disjuntos. Por otra parte, construyendo sobre la noción de cotas ajustadas para campos de la técnica TACO, presentamos MUCHO-TACO, una técnica para distribuir la verificación de programas Java anotados con contratos JML, basada en la herramienta secuencial TACO. Por último presentamos BLISS, un conjunto de técnicas para refinar la búsqueda de estructuras válidas durante la ejecución simbólica, basadas en Symbolic PathFinder.Palabras clave – provistas por el repositorio digital
INGENIERIA DE SOFTWARE; ANALISIS AUTOMATICO DE SOFTWARE; VERIFICACION EXHAUSTIVA ACOTADA; SISTEMAS DISTRIBUIDOS; EJECUCION SIMBOLICA; ALLOY; JAVA (LENGUAJE DE PROGRAMACION); JML; TACO; SOFTWARE ENGINEERING; AUTOMATED SOFTWARE ANALYSIS; BOUNDED EXHAUSTIVE VERIFICATION; DISTRIBUTED SYSTEMS; SYMBOLIC EXECUTION; JAVA
Disponibilidad
| Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
|---|---|---|---|---|
| No requiere | 2015 | Biblioteca Digital (FCEN-UBA) (SNRD) |
|
Información
Tipo de recurso:
tesis
Idiomas de la publicación
- español castellano
País de edición
Argentina
Fecha de publicación
2015-12-15
Información sobre licencias CC
