Técnicas distribuídas para verificación acotada eficiente

Mostrar todas las versiones(3)

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. Losmétodos livianos son más fáciles de aprender y se materializan en herramientas totalmente...

Descripción completa

Detalles Bibliográficos
Autor principal:	Rosner, Nicolás Leandro
Otros Autores:	Frias, Marcelo Fabián
Formato:	Tesis doctoral publishedVersion
Lenguaje:	Inglés
Publicado:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2015
Materias:	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
Acceso en línea:	https://hdl.handle.net/20.500.12110/tesis_n6011_Rosner https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6011_Rosner_oai
Aporte de:	Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires

id	I28-R145-tesis_n6011_Rosner_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	Inglés
orig_language_str_mv	eng
topic	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 ALLOY JAVA JML TACO
spellingShingle	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 ALLOY JAVA JML TACO Rosner, Nicolás Leandro Técnicas distribuídas para verificación acotada eficiente
topic_facet	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 ALLOY JAVA JML TACO
description	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. Losmé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 exhaustivaacotada, la validez del resultado devuelto por la herramienta automática siempre está limitada poralguna noción de alcance o tamaño máximo configurable por el usuario. Para incrementar el grado deconfianza 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 dichoalcance. En esta tesis presentamos una serie de técnicas y herramientas cuyo objetivo es mejorar la escalabilidaddel análisis exhaustivo acotado de artefactos de software. En particular, nos interesa poderaprovechar la disponibilidad de hardware de bajo costo (como por ejemplo clusters de PCs, existentesen muchas empresas e instituciones) para extender la frontera de lo tratable mediante esta clase deenfoques. 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 asistirla toma automática de decisiones en tamaños mayores del mismo problema. Mostramos su aplicaciónal análisis distribuido de modelos Alloy, así como a la toma de decisiones en la generación de casos detest 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 potencialescontraejemplos 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 anotadoscon contratos JML, basada en la herramienta secuencial TACO. Por último presentamos BLISS, un conjunto de técnicas para refinar la búsqueda de estructurasválidas durante la ejecución simbólica, basadas en Symbolic PathFinder.
author2	Frias, Marcelo Fabián
author_facet	Frias, Marcelo Fabián Rosner, Nicolás Leandro
format	Tesis doctoral Tesis doctoral publishedVersion
author	Rosner, Nicolás Leandro
author_sort	Rosner, Nicolás Leandro
title	Técnicas distribuídas para verificación acotada eficiente
title_short	Técnicas distribuídas para verificación acotada eficiente
title_full	Técnicas distribuídas para verificación acotada eficiente
title_fullStr	Técnicas distribuídas para verificación acotada eficiente
title_full_unstemmed	Técnicas distribuídas para verificación acotada eficiente
title_sort	técnicas distribuídas para verificación acotada eficiente
publisher	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate	2015
url	https://hdl.handle.net/20.500.12110/tesis_n6011_Rosner https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6011_Rosner_oai
work_keys_str_mv	AT rosnernicolasleandro tecnicasdistribuidasparaverificacionacotadaeficiente AT rosnernicolasleandro distributedtechniquesforefficientboundedverification
_version_	1824355773906419712
spelling	I28-R145-tesis_n6011_Rosner_oai2024-09-02 Frias, Marcelo Fabián Rosner, Nicolás Leandro 2015-12-15 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. Losmé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 exhaustivaacotada, la validez del resultado devuelto por la herramienta automática siempre está limitada poralguna noción de alcance o tamaño máximo configurable por el usuario. Para incrementar el grado deconfianza 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 dichoalcance. En esta tesis presentamos una serie de técnicas y herramientas cuyo objetivo es mejorar la escalabilidaddel análisis exhaustivo acotado de artefactos de software. En particular, nos interesa poderaprovechar la disponibilidad de hardware de bajo costo (como por ejemplo clusters de PCs, existentesen muchas empresas e instituciones) para extender la frontera de lo tratable mediante esta clase deenfoques. 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 asistirla toma automática de decisiones en tamaños mayores del mismo problema. Mostramos su aplicaciónal análisis distribuido de modelos Alloy, así como a la toma de decisiones en la generación de casos detest 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 potencialescontraejemplos 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 anotadoscon contratos JML, basada en la herramienta secuencial TACO. Por último presentamos BLISS, un conjunto de técnicas para refinar la búsqueda de estructurasválidas durante la ejecución simbólica, basadas en Symbolic PathFinder. Formal analysis of software artifacts is often divided into two kinds of methods: heavyweight andlightweight. The former offer complete certainty in the result, but require interaction with highlytrained expert users. The latter are easier to learn and supported by fully automated tools, but thevalidity of their results is typically partial. For instance, in bounded exhaustive analysis techniques,the validity of the result is always limited by some notion of scope or maximum size provided bythe user. To increase the level of confidence of the result, the user can simply increase the scope ofthe analysis and run the tool again. However, the computational cost of such automated analyses isalmost always exponential in said scope. In this thesis we present a series of techniques and tools with the common goal of improving thescalability of bounded exhaustive analysis of software artifacts. In particular, we are interested inleveraging the availability of low-cost hardware (such as PC clusters, which are currently availablein many companies and institutions) in order to push the tractability barrier of bounded exhaustiveanalysis techniques. We present transcoping, an incremental approach that explores bounded exhaustive verificationproblems at small sizes, gathers information, then extrapolates it in order to make better-informeddecisions at larger sizes of the same problems. We show its application to the distributed analysis of Alloy models, as well as to the generation of bounded exhaustive test suites using hybrid invariants. We then present Ranger, another technique to distribute the analysis of Alloy models which splitsthe problem into subproblems of lower complexity by linearizing the space of potential counterexamplesand dividing it into disjoint intervals. Building on the notion of tight field bounds from the TACO technique, we present MUCHO-TACO,a technique for distributed verification of Java programs annotated with JML contracts, based on thesequential TACO tool. We also present BLISS, a set of techniques to improve the search for valid structures during symbolicexecution for non-primitive inputs based on Symbolic PathFinder. Fil: Rosner, Nicolás Leandro. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/tesis_n6011_Rosner eng 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 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 ALLOY JAVA JML TACO Técnicas distribuídas para verificación acotada eficiente Distributed techniques for efficient bounded verification info:eu-repo/semantics/doctoralThesis info:ar-repo/semantics/tesis doctoral info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6011_Rosner_oai

Técnicas distribuídas para verificación acotada eficiente

Ejemplares similares