Tesis > Documento


Ver el documento (formato PDF)   Galeotti, Juan Pablo.  "Verificación de software usando Alloy"  (2010)
Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
URL:
     
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.

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

Registro:
Título : Verificación de software usando Alloy     =    Software verification using Alloy
Autor : Galeotti, Juan Pablo
Director : Frias, Marcelo Fabián
Consejero : Braberman, Victor
Jurados : Olivero, A.  ; Marinov, D.  ; Jackson, D.
Año : 2010
Editor : Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
Filiación : Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
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_4781_Galeotti
Idioma : Inglés
Area Temática : Computación / Ingeniería del Software
Palabras claves : VERIFICACION; LENGUAJES; ANALISIS ESTATICO; ANALISIS DE PROGRAMAS USANDO SAT; ALLOY; KODKOD; DYNALLOY; VERIFICATION; LANGUAGES; STATIC ANALYSIS; SAT-BASED CODE ANALYSIS; ALLOY; KODKOD; DYNALLOY
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