Tesis > Documento


Ver el documento (formato PDF)   Moscato, Mariano Miguel.  "Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving"  (2013)
Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
URL:
     
Resumen:
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.

Abstract:
Formal analysis of software models can be undertaken following two approaches: the lightweight and the heavyweight. The former offers languages with simple syntax and semantics, supported by automatic analysis tools. Nevertheless, the analysis they perform is usually partial. The latter provides full confidence analysis of models, but often requires interaction from highly trained users. Alloy is a good example of a lightweight method. Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off- the-shelf SAT-solvers. The translation requires user-provided bounds on the sizes of data domains. The analysis is limited by the bounds, and is therefore partial. Thus, the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive results are necessary. In this thesis we develop Dynamite, an extension of PVS that embeds a complete calculus for Alloy. PVS is a well-known heavyweight method. It provides a semi-automatic theorem prover for higher order logic. Dynamite complements the partial automatic analysis offered by the Alloy Analyzer with semi-automatic verification through theorem proving. It also improves the theorem proving experience by using the Alloy Analyzer to provide automatic functionality intended for early detection of errors, proof refinement and witness generation for existentially quantified properties.

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

Registro:
Título : Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving     =    Improvements to interactive theorem proving of alloy properties using sat-solving
Autor : Moscato, Mariano Miguel
Director : Frias, Marcelo Fabián
Consejero : López Pombo, Carlos Gustavo
Jurados : Areces, Carlos Eduardo  ; Jackson, Daniel N.  ; Shankar, Natarajan
Año : 2013
Editor : Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
Filiación : Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Departamento de Computación
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_5428_Moscato
Idioma : Inglés
Area Temática : Computación / Ingeniería del Software
Computación / Lenguajes y Sistemas Informáticos
Palabras claves : DEMOSTRACION DE TEOREMAS INTERACTIVA; SAT-SOLVING; CALCULO PARA ALLOY; PVS; ANALISIS DE ESPECIFICACIONES DE SOFTWARE; INTERACTIVE THEOREM PROVING; SAT-SOLVING; ALLOY CALCULUS; PVS; SPECIFICATION ANALYSIS
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