Verificación de software usando Alloy

Institución otorgante:

Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales

Fecha:

2010

Tipo de documento: 

info:eu-repo/semantics/doctoralThesis
 

Formato:

application/pdf

Idioma:

eng

Temas:

VERIFICACION - LENGUAJES - ANALISIS ESTATICO - ANALISIS DE PROGRAMAS USANDO SAT - ALLOY - KODKOD - DYNALLOY - VERIFICATION - LANGUAGES - STATIC ANALYSIS - SAT-BASED CODE ANALYSIS - ALLOY - KODKOD - DYNALLOY

Descripción:

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.

Identificador:

https://hdl.handle.net/20.500.12110/tesis_n4781_Galeotti