Verificación de software usando Alloy

Mostrar todas las versiones(3)

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 encontr...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Galeotti, Juan Pablo
Otros Autores:	Frias, Marcelo Fabián
Formato:	Tesis doctoral publishedVersion
Lenguaje:	Inglés
Publicado:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2010
Materias:	VERIFICACION LENGUAJES ANALISIS ESTATICO ANALISIS DE PROGRAMAS USANDO SAT ALLOY KODKOD DYNALLOY VERIFICATION LANGUAGES STATIC ANALYSIS SAT-BASED CODE ANALYSIS
Acceso en línea:	https://hdl.handle.net/20.500.12110/tesis_n4781_Galeotti
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	tesis:tesis_n4781_Galeotti
record_format	dspace
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language	Inglés
orig_language_str_mv	eng
topic	VERIFICACION LENGUAJES ANALISIS ESTATICO ANALISIS DE PROGRAMAS USANDO SAT ALLOY KODKOD DYNALLOY VERIFICATION LANGUAGES STATIC ANALYSIS SAT-BASED CODE ANALYSIS ALLOY KODKOD DYNALLOY
spellingShingle	VERIFICACION LENGUAJES ANALISIS ESTATICO ANALISIS DE PROGRAMAS USANDO SAT ALLOY KODKOD DYNALLOY VERIFICATION LANGUAGES STATIC ANALYSIS SAT-BASED CODE ANALYSIS ALLOY KODKOD DYNALLOY Galeotti, Juan Pablo Verificación de software usando Alloy
topic_facet	VERIFICACION LENGUAJES ANALISIS ESTATICO ANALISIS DE PROGRAMAS USANDO SAT ALLOY KODKOD DYNALLOY VERIFICATION LANGUAGES STATIC ANALYSIS SAT-BASED CODE ANALYSIS ALLOY KODKOD DYNALLOY
description	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.
author2	Frias, Marcelo Fabián
author_facet	Frias, Marcelo Fabián Galeotti, Juan Pablo
format	Tesis doctoral Tesis doctoral publishedVersion
author	Galeotti, Juan Pablo
author_sort	Galeotti, Juan Pablo
title	Verificación de software usando Alloy
title_short	Verificación de software usando Alloy
title_full	Verificación de software usando Alloy
title_fullStr	Verificación de software usando Alloy
title_full_unstemmed	Verificación de software usando Alloy
title_sort	verificación de software usando alloy
publisher	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate	2010
url	https://hdl.handle.net/20.500.12110/tesis_n4781_Galeotti
work_keys_str_mv	AT galeottijuanpablo verificaciondesoftwareusandoalloy AT galeottijuanpablo softwareverificationusingalloy
_version_	1782022812420014080
spelling	tesis:tesis_n4781_Galeotti2023-10-02T20:00:49Z Verificación de software usando Alloy Software verification using Alloy Galeotti, Juan Pablo Frias, Marcelo Fabián VERIFICACION LENGUAJES ANALISIS ESTATICO ANALISIS DE PROGRAMAS USANDO SAT ALLOY KODKOD DYNALLOY VERIFICATION LANGUAGES STATIC ANALYSIS SAT-BASED CODE ANALYSIS ALLOY KODKOD DYNALLOY 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. 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. Fil: Galeotti, Juan Pablo. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2010 info:eu-repo/semantics/doctoralThesis info:ar-repo/semantics/tesis doctoral info:eu-repo/semantics/publishedVersion application/pdf eng info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/tesis_n4781_Galeotti

Verificación de software usando Alloy

Ejemplares similares