Catálogo de publicaciones - tesis
Título de Acceso Abierto
Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving
Mariano Miguel Moscato Marcelo Fabián Frias
publishedVersion.
Resumen/Descripción – provisto por el repositorio digital
El análisis formal de especificaciones de software suele atacarse desde dos enfoques, usualmente llamados: liviano y pesado. En el lado liviano encontramos lenguajes fáciles de aprender y utilizar junto con herramientas automáticas de análisis, pero de alcance parcial. El lado pesado nos ofrece lograr certeza absoluta, pero a costo de requerir usuarios altamente capacitados. Un buen representante de los métodos livianos es lenguaje de modelado Alloy y su analizador automático: el Alloy Analyzer. Su análisis consiste en transcribir un modelo Alloy a una fórmula proposicional que luego se procesa utilizando SAT-solvers estándar. Esta transcripción requiere que el usuario establezca cotas en los tamaños de los dominios modelados en la especificación. El análisis, entonces, es parcial, ya que está limitado por esas cotas. Por ello, puede pensarse que no es seguro utilizar el Alloy Analyzer para trabajar en el desarrollo de aplicaciones críticas donde se necesitan resultados concluyentes. En esta tesis presentamos un cálculo basado en álgebras de Fork que permite realizar demostraciones en cálculo de secuentes sobre especificaciones Alloy. También hemos desarrollado una herramienta (Dynamite) que lo implementa. Dynamite es una extensión del sistema de demostración semiatomático PVS, método pesado ampliamente utilizado por la comunidad. Así, Dynamite consigue complementar el análisis parcial que ofrece Alloy, además de potenciar el esfuerzo realizado durante una demostración usando el Alloy Analyzer para detectar errores tempranamente, refinar secuentes y proponer términos para utilizar como testigos de propiedades cuantificadas existencialmente.Palabras clave – provistas por el repositorio digital
DEMOSTRACION DE TEOREMAS INTERACTIVA; SAT-SOLVING; CALCULO PARA ALLOY; PVS; ANALISIS DE ESPECIFICACIONES DE SOFTWARE; INTERACTIVE THEOREM PROVING; ALLOY CALCULUS; SPECIFICATION ANALYSIS
Disponibilidad
| Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
|---|---|---|---|---|
| No requiere | 2013 | Biblioteca Digital (FCEN-UBA) (SNRD) |
|
Información
Tipo de recurso:
tesis
Idiomas de la publicación
- español castellano
País de edición
Argentina
Fecha de publicación
2013
Información sobre licencias CC
