Registro:
| Documento: | Tesis Doctoral |
| Disciplina: | computacion |
| Título: | Verificación de software usando Alloy |
| Título alternativo: | Software verification using Alloy |
| Autor: | Galeotti, Juan Pablo |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la Web: | 2011-05-09 |
| Fecha de defensa: | 2010 |
| Fecha en portada: | 2010 |
| Grado Obtenido: | Doctorado |
| Título Obtenido: | Doctor de la Universidad de Buenos Aires en el área de Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Frias, Marcelo Fabián |
| Consejero: | Braberman, Víctor Adrián |
| Jurado: | Olivero, Alfredo; Marinov, Darko; Jackson, Daniel N. |
| Idioma: | Inglés |
| Palabras clave: | VERIFICACION; LENGUAJES; ANALISIS ESTATICO; ANALISIS DE PROGRAMAS USANDO SAT; ALLOY; KODKOD; DYNALLOYVERIFICATION; LANGUAGES; STATIC ANALYSIS; SAT-BASED CODE ANALYSIS; ALLOY; KODKOD; DYNALLOY |
| Tema: | computación/ingeniería del software
|
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/tesis_n4781_Galeotti |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n4781_Galeotti.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/tesis/document/tesis_n4781_Galeotti |
| Ubicación: | COM 004781 |
| 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. Galeotti, Juan Pablo. (2010). Verificación de software usando Alloy. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales). Recuperado de http://hdl.handle.net/20.500.12110/tesis_n4781_Galeotti |
Resumen:
La verificación acotada de software usando SAT consiste en la traducción del programa junto con las anotaciones provistas por el usuario a una fórmula proposicional. Luego de lo cual la fórmula es analizada en busca de violaciones a la especificación usando un SAT-solver. Si una violación es encontrada, una traza de ejecución exponiendo el error es exhibida al usuario. Alloy es un lenguaje formal relacional que nos permite automáticamente analizar especificiaciones buscando contraejemplos de aserciones con la ayuda de un SAT-solver off-the-shelf. Las contribuciones de la presente tesis son principalmente dos. Por un lado, se presenta una traducción desde software anotado en lenguaje JML al lenguaje Alloy. Para conseguir esto, se presenta: • DynAlloy, una extensión al lenguaje de especificación Alloy para describir propiedades dinámicas de los sistemas usando acciones. Extendemos la sintaxis de Alloy con una notación para escribir aserciones de correctitud parcial. La semántica de estas aserciones es una adaptación del precondición liberal más débil de Dijsktra. • DynJML, un lenguaje de especificación orientado a objetos que sirve de representación intermedia para facilitar la traducción de JML a DynAlloy. • TACO, un prototipo que implementa la traducción de JML a DynAlloy. En segundo lugar, introducimos una técnica novedosa, general y complementamente automatizable para analizar programas Java secuenciales anotados con JML usando SAT. Esta técnica es especialmente beneficiosa cuando el programa opera con estructuras de datos complejas. Para esto, se instrumenta el modelo Alloy con un predicado de ruptura de simetrías que nos permite el cómputo paralelo y automatizado de cotas ajustadas para los campos Java.
Abstract:
SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and an- alyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Alloy is a formal specification language that allows us to automatically ana- lyze specifications by searching for counterexamples of assertions with the help of the off-the-shelf SAT solvers. The contributions of this dissertation are twofold. Firstly, we present a trans- lation from Java Modelling Language (a behavioural specification language for Java) to Alloy. In order to do so, we introduce: • DynAlloy, an extension to the Alloy specification language to describe dynamic properties of systems using actions. We extend Alloy’s syntax with a notation for partial correctness assertions, whose semantics relies on an adaptation of Dijkstra’s weakest liberal precondition. • DynJML, an intermediate object-oriented specification language to allevi- ate the burden of translating JML to DynAlloy. • TACO, a prototype tool which implements the entire tool-chain. Secondly, we introduce a novel, general and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument Alloy with a symmetry-breaking predicate that allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading to a speedup on the analysis of orders of magnitude compared to the non-instrumented SAT-based analysis.
Citación:
---------- APA ----------
Galeotti, Juan Pablo. (2010). Verificación de software usando Alloy. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/tesis_n4781_Galeotti
---------- CHICAGO ----------
Galeotti, Juan Pablo. "Verificación de software usando Alloy". Tesis Doctoral, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2010.https://hdl.handle.net/20.500.12110/tesis_n4781_Galeotti
Estadísticas:
Descargas totales desde :
Descargas mensuales
https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n4781_Galeotti.pdf
