Registro:
| Documento: | Tesis Doctoral |
| Disciplina: | computacion |
| Título: | Técnicas distribuídas para verificación acotada eficiente |
| Título alternativo: | Distributed techniques for efficient bounded verification |
| Autor: | Rosner, Nicolás Leandro |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Filiación: | Departamento de Computación
|
| Publicación en la Web: | 2016-09-02 |
| Fecha de defensa: | 2015-12-15 |
| Fecha en portada: | 2015 |
| Grado Obtenido: | Doctorado |
| Título Obtenido: | Doctor de la Universidad de Buenos Aires en el área de Ciencias de la Computación |
| Director: | Frias, Marcelo Fabián |
| Consejero: | López Pombo, Carlos Gustavo |
| Jurado: | Elbaum, Sebastián; Fischer, Bernd; Uchitel, Sebastián |
| Idioma: | Inglés |
| Palabras clave: | INGENIERIA DE SOFTWARE; ANALISIS AUTOMATICO DE SOFTWARE; VERIFICACION EXHAUSTIVA ACOTADA; SISTEMAS DISTRIBUIDOS; EJECUCION SIMBOLICA; ALLOY; JAVA (LENGUAJE DE PROGRAMACION); JML; TACOSOFTWARE ENGINEERING; AUTOMATED SOFTWARE ANALYSIS; BOUNDED EXHAUSTIVE VERIFICATION; DISTRIBUTED SYSTEMS; SYMBOLIC EXECUTION; ALLOY; JAVA; JML; TACO |
| Tema: | computación/ingeniería del software
|
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/tesis_n6011_Rosner |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n6011_Rosner.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/tesis/document/tesis_n6011_Rosner |
| Ubicación: | Dep.COM 006011 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Rosner, Nicolás Leandro. (2015). Técnicas distribuídas para verificación acotada eficiente. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/tesis_n6011_Rosner |
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. 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.
Abstract:
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.
Citación:
---------- APA ----------
Rosner, Nicolás Leandro. (2015). Técnicas distribuídas para verificación acotada eficiente. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/tesis_n6011_Rosner
---------- CHICAGO ----------
Rosner, Nicolás Leandro. "Técnicas distribuídas para verificación acotada eficiente". Tesis Doctoral, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2015.https://hdl.handle.net/20.500.12110/tesis_n6011_Rosner
Estadísticas:
Descargas totales desde :
Descargas mensuales
https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n6011_Rosner.pdf
