Tesis > Documento


Ver el documento (formato PDF)   Rosner, Nicolás Leandro.  "Técnicas distribuídas para verificación acotada eficiente"  (2015-12-15)
Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
URL:
     
Resumen:
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.

Abstract:
Formal analysis of software artifacts is often divided into two kinds of methods: heavyweight and lightweight. The former offer complete certainty in the result, but require interaction with highly trained expert users. The latter are easier to learn and supported by fully automated tools, but the validity 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 by the user. To increase the level of confidence of the result, the user can simply increase the scope of the analysis and run the tool again. However, the computational cost of such automated analyses is almost always exponential in said scope. In this thesis we present a series of techniques and tools with the common goal of improving the scalability of bounded exhaustive analysis of software artifacts. In particular, we are interested in leveraging the availability of low-cost hardware (such as PC clusters, which are currently available in many companies and institutions) in order to push the tractability barrier of bounded exhaustive analysis techniques. We present transcoping, an incremental approach that explores bounded exhaustive verification problems at small sizes, gathers information, then extrapolates it in order to make better-informed decisions 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 splits the problem into subproblems of lower complexity by linearizing the space of potential counterexamples and 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 the sequential TACO tool. We also present BLISS, a set of techniques to improve the search for valid structures during symbolic execution for non-primitive inputs based on Symbolic PathFinder.

* A este resumen le pueden faltar caracteres especiales. Consulte la versión completa en el documento en formato PDF

Registro:
Título : Técnicas distribuídas para verificación acotada eficiente     =    Distributed techniques for efficient bounded verification
Autor : Rosner, Nicolás Leandro
Director : Frias, Marcelo Fabián
Consejero : López Pombo, Carlos Gustavo
Jurados : Elbaum, Sebastián  ; Fischer, Bernd  ; Uchitel, Sebastián
Año : 2015-12-15
Editor : Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
Filiación : Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Departamento de Computación
Grado obtenido : Doctor de la Universidad de Buenos Aires en el área de Ciencias de la Computación
Ubicación : Preservación - http://digital.bl.fcen.uba.ar/gsdl-282/cgi-bin/library.cgi?a=d&c=tesis&d=Tesis_6011_Rosner
Idioma : Inglés
Area Temática : Computación / Ingeniería del Software
Palabras claves : 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
URL al Documento : 
URL al Registro : 
hola chau _gs.DocumentHeader_ chau2 _documentheader_ chau3
Estadísticas:
     http://digital.bl.fcen.uba.ar
Biblioteca Central Dr. Luis Federico Leloir - Facultad de Ciencias Exactas y Naturales - Universidad de Buenos Aires
Intendente Güiraldes 2160 - Ciudad Universitaria - Pabellón II - C1428EGA - Tel. (54 11) 4789-9293 int 34