Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving

Mostrar todas las versiones(3)

El análisis formal de especificaciones de software suele atacarse desde dosenfoques, usualmente llamados: liviano y pesado. En el lado liviano encontramoslenguajes fáciles de aprender y utilizar junto con herramientasautomáticas de análisis, pero de alcance parcial. El lado pesado nos ofrecelograr c...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Moscato, Mariano Miguel
Formato:	Tesis Doctoral
Lenguaje:	Inglés
Publicado:	2013
Materias:	DEMOSTRACION DE TEOREMAS INTERACTIVA SAT-SOLVING CALCULO PARA ALLOY PVS ANALISIS DE ESPECIFICACIONES DE SOFTWARE INTERACTIVE THEOREM PROVING ALLOY CALCULUS SPECIFICATION ANALYSIS
Acceso en línea:	https://hdl.handle.net/20.500.12110/tesis_n5428_Moscato
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:tesis_n5428_Moscato
record_format	dspace
spelling	todo:tesis_n5428_Moscato2023-10-03T12:57:06Z Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving Improvements to interactive theorem proving of alloy properties using sat-solving Moscato, Mariano Miguel 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 El análisis formal de especificaciones de software suele atacarse desde dosenfoques, usualmente llamados: liviano y pesado. En el lado liviano encontramoslenguajes fáciles de aprender y utilizar junto con herramientasautomáticas de análisis, pero de alcance parcial. El lado pesado nos ofrecelograr 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 consisteen transcribir un modelo Alloy a una fórmula proposicional que luego seprocesa utilizando SAT-solvers estándar. Esta transcripción requiere que el usuario establezca cotas en los tamañosde los dominios modelados en la especificación. El análisis, entonces, esparcial, ya que está limitado por esas cotas. Por ello, puede pensarse queno es seguro utilizar el Alloy Analyzer para trabajar en el desarrollo deaplicaciones críticas donde se necesitan resultados concluyentes. En esta tesis presentamos un cálculo basado en álgebras de Fork que permiterealizar demostraciones en cálculo de secuentes sobre especificaciones Alloy. También hemos desarrollado una herramienta (Dynamite) que loimplementa. 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 usandoel Alloy Analyzer para detectar errores tempranamente, refinar secuentes yproponer términos para utilizar como testigos de propiedades cuantificadasexistencialmente. Formal analysis of software models can be undertaken following two approaches:the lightweight and the heavyweight. The former offers languageswith simple syntax and semantics, supported by automatic analysis tools. Nevertheless, the analysis they perform is usually partial. The latter providesfull confidence analysis of models, but often requires interaction fromhighly trained users. Alloy is a good example of a lightweight method. Automatic analysisof Alloy models is supported by the Alloy Analyzer, a tool that translatesan Alloy model to a propositional formula that is then analyzed using off-the-shelf SAT-solvers. The translation requires user-provided bounds on thesizes of data domains. The analysis is limited by the bounds, and is thereforepartial. Thus, the Alloy Analyzer may not be appropriate for the analysisof critical applications where more conclusive results are necessary. In this thesis we develop Dynamite, an extension of PVS that embeds acomplete calculus for Alloy. PVS is a well-known heavyweight method. Itprovides a semi-automatic theorem prover for higher order logic. Dynamitecomplements the partial automatic analysis offered by the Alloy Analyzerwith semi-automatic verification through theorem proving. It also improvesthe theorem proving experience by using the Alloy Analyzer to provide automaticfunctionality intended for early detection of errors, proof refinementand witness generation for existentially quantified properties. Fil: Moscato, Mariano Miguel. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2013 Tesis Doctoral PDF Inglés info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/tesis_n5428_Moscato
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	Inglés
topic	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
spellingShingle	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 Moscato, Mariano Miguel Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving
topic_facet	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
description	El análisis formal de especificaciones de software suele atacarse desde dosenfoques, usualmente llamados: liviano y pesado. En el lado liviano encontramoslenguajes fáciles de aprender y utilizar junto con herramientasautomáticas de análisis, pero de alcance parcial. El lado pesado nos ofrecelograr 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 consisteen transcribir un modelo Alloy a una fórmula proposicional que luego seprocesa utilizando SAT-solvers estándar. Esta transcripción requiere que el usuario establezca cotas en los tamañosde los dominios modelados en la especificación. El análisis, entonces, esparcial, ya que está limitado por esas cotas. Por ello, puede pensarse queno es seguro utilizar el Alloy Analyzer para trabajar en el desarrollo deaplicaciones críticas donde se necesitan resultados concluyentes. En esta tesis presentamos un cálculo basado en álgebras de Fork que permiterealizar demostraciones en cálculo de secuentes sobre especificaciones Alloy. También hemos desarrollado una herramienta (Dynamite) que loimplementa. 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 usandoel Alloy Analyzer para detectar errores tempranamente, refinar secuentes yproponer términos para utilizar como testigos de propiedades cuantificadasexistencialmente.
format	Tesis Doctoral
author	Moscato, Mariano Miguel
author_facet	Moscato, Mariano Miguel
author_sort	Moscato, Mariano Miguel
title	Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving
title_short	Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving
title_full	Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving
title_fullStr	Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving
title_full_unstemmed	Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving
title_sort	mejoras a la demostración interactiva de propiedades alloy utilizando sat-solving
publishDate	2013
url	https://hdl.handle.net/20.500.12110/tesis_n5428_Moscato
work_keys_str_mv	AT moscatomarianomiguel mejorasalademostracioninteractivadepropiedadesalloyutilizandosatsolving AT moscatomarianomiguel improvementstointeractivetheoremprovingofalloypropertiesusingsatsolving
_version_	1782025475101556736

Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving

Ejemplares similares