ParAlloy una implementación paralelay distribuida para DynAlloy

Mostrar todas las versiones(3)

Los métodos formales livianos (lightweight) suelen considerarse preferibles en ciertos contextos debido a que reducen los requerimientos de entrenamiento formal sobre los ingenieros de software que los utilizan. Esta ventaja, sin embargo, no es gratuita: los métodos livianos suelen ser limitados, ya...

Descripción completa

Detalles Bibliográficos
Autor principal: Rosner, Nicolás
Otros Autores: Frias, Marcelo Fabián
Formato: Tesis de grado publishedVersion
Lenguaje:Español
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2006
Materias:
ALLOY
DYNALLOY
PARALLOY
VERIFICACION DE PROPIEDADES
DEMOSTRACION (SEMI) AUTOMATICA DE TEOREMAS
METODOS FORMALES (RELACIONALES)
SISTEMAS DISTRIBUIDOS
PROGRAMACION PARALELA
JINI
JAVASPACES
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000302_Rosner
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000302_Rosner_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-seminario_nCOM000302_Rosner_oai
record_format dspace
spelling I28-R145-seminario_nCOM000302_Rosner_oai2024-12-17 Frias, Marcelo Fabián López Pombo, Carlos Gustavo Rosner, Nicolás 2006 Los métodos formales livianos (lightweight) suelen considerarse preferibles en ciertos contextos debido a que reducen los requerimientos de entrenamiento formal sobre los ingenieros de software que los utilizan. Esta ventaja, sin embargo, no es gratuita: los métodos livianos suelen ser limitados, ya sea en su capacidad expresiva o en la tratabilidad de problemas grandes, dada la extensa cantidad de recursos que el análisis automático puede requerir. Alloy es un buen ejemplo de método formal liviano. El lenguaje de modelado Alloy permite especificar sistemas en un dialecto de la lógica relacional, que a su vez es una extensión de la lógica de primer orden. La herramienta Alloy Analyzer permite verificar propiedades sobre esos sistemas; lo hace por reducción a un problema SAT, acotando el tamaño de los dominios para poder lograr un análisis efectivo y correcto (dentro de ciertos scopes). DynAlloy extiende a Alloy mediante un lenguaje que permite especificar acciones atómicas y programas (acciones compuestas por otras acciones), una semántica de entrada/salida bien definida, y la posibilidad de aseverar propiedades acerca de un programa bajo la forma de partial correctness assertions. La herramienta DynAlloy permite traducir especificaciones DynAlloy al lenguaje Alloy, para su posterior análisis mediante Alloy Analyzer. Nuestra experiencia indica que el análisis de modelos Alloy requiere mucho tiempo, y que esto sólo tiende a empeorar cuando se trata de modelos provenientes de especificaciones DynAlloy que involucran acciones complejas. En el artículo introductorio a DynAlloy se deja planteada, como trabajo futuro, una hipótesis según la cual la estructura de las fórmulas resultantes de la traducción DynAlloy −→ Alloy es susceptible de ser eficientemente analizada en paralelo. Nuestro trabajo consistió en poner a prueba dicha hipótesis, en parte mediante el análisis teórico, en parte en forma experimental a través del desarrollo de ParAlloy, una implementación paralela y distribuida de DynAlloy, cuya primera versión operativa y documentación de diseño se presentan junto con el presente informe. Fil: Rosner, Nicolás. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000302_Rosner spa Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar ALLOY DYNALLOY PARALLOY VERIFICACION DE PROPIEDADES DEMOSTRACION (SEMI) AUTOMATICA DE TEOREMAS METODOS FORMALES (RELACIONALES) SISTEMAS DISTRIBUIDOS PROGRAMACION PARALELA JINI JAVASPACES ParAlloy una implementación paralelay distribuida para DynAlloy info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000302_Rosner_oai
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (UBA)
language Español
orig_language_str_mv spa
topic ALLOY
DYNALLOY
PARALLOY
VERIFICACION DE PROPIEDADES
DEMOSTRACION (SEMI) AUTOMATICA DE TEOREMAS
METODOS FORMALES (RELACIONALES)
SISTEMAS DISTRIBUIDOS
PROGRAMACION PARALELA
JINI
JAVASPACES
spellingShingle ALLOY
DYNALLOY
PARALLOY
VERIFICACION DE PROPIEDADES
DEMOSTRACION (SEMI) AUTOMATICA DE TEOREMAS
METODOS FORMALES (RELACIONALES)
SISTEMAS DISTRIBUIDOS
PROGRAMACION PARALELA
JINI
JAVASPACES
Rosner, Nicolás
ParAlloy una implementación paralelay distribuida para DynAlloy
topic_facet ALLOY
DYNALLOY
PARALLOY
VERIFICACION DE PROPIEDADES
DEMOSTRACION (SEMI) AUTOMATICA DE TEOREMAS
METODOS FORMALES (RELACIONALES)
SISTEMAS DISTRIBUIDOS
PROGRAMACION PARALELA
JINI
JAVASPACES
description Los métodos formales livianos (lightweight) suelen considerarse preferibles en ciertos contextos debido a que reducen los requerimientos de entrenamiento formal sobre los ingenieros de software que los utilizan. Esta ventaja, sin embargo, no es gratuita: los métodos livianos suelen ser limitados, ya sea en su capacidad expresiva o en la tratabilidad de problemas grandes, dada la extensa cantidad de recursos que el análisis automático puede requerir. Alloy es un buen ejemplo de método formal liviano. El lenguaje de modelado Alloy permite especificar sistemas en un dialecto de la lógica relacional, que a su vez es una extensión de la lógica de primer orden. La herramienta Alloy Analyzer permite verificar propiedades sobre esos sistemas; lo hace por reducción a un problema SAT, acotando el tamaño de los dominios para poder lograr un análisis efectivo y correcto (dentro de ciertos scopes). DynAlloy extiende a Alloy mediante un lenguaje que permite especificar acciones atómicas y programas (acciones compuestas por otras acciones), una semántica de entrada/salida bien definida, y la posibilidad de aseverar propiedades acerca de un programa bajo la forma de partial correctness assertions. La herramienta DynAlloy permite traducir especificaciones DynAlloy al lenguaje Alloy, para su posterior análisis mediante Alloy Analyzer. Nuestra experiencia indica que el análisis de modelos Alloy requiere mucho tiempo, y que esto sólo tiende a empeorar cuando se trata de modelos provenientes de especificaciones DynAlloy que involucran acciones complejas. En el artículo introductorio a DynAlloy se deja planteada, como trabajo futuro, una hipótesis según la cual la estructura de las fórmulas resultantes de la traducción DynAlloy −→ Alloy es susceptible de ser eficientemente analizada en paralelo. Nuestro trabajo consistió en poner a prueba dicha hipótesis, en parte mediante el análisis teórico, en parte en forma experimental a través del desarrollo de ParAlloy, una implementación paralela y distribuida de DynAlloy, cuya primera versión operativa y documentación de diseño se presentan junto con el presente informe.
author2 Frias, Marcelo Fabián
author_facet Frias, Marcelo Fabián
Rosner, Nicolás
format Tesis de grado
Tesis de grado
publishedVersion
author Rosner, Nicolás
author_sort Rosner, Nicolás
title ParAlloy una implementación paralelay distribuida para DynAlloy
title_short ParAlloy una implementación paralelay distribuida para DynAlloy
title_full ParAlloy una implementación paralelay distribuida para DynAlloy
title_fullStr ParAlloy una implementación paralelay distribuida para DynAlloy
title_full_unstemmed ParAlloy una implementación paralelay distribuida para DynAlloy
title_sort paralloy una implementación paralelay distribuida para dynalloy
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2006
url https://hdl.handle.net/20.500.12110/seminario_nCOM000302_Rosner
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000302_Rosner_oai
work_keys_str_mv AT rosnernicolas paralloyunaimplementacionparalelaydistribuidaparadynalloy
_version_ 1824952622604353536

Ejemplares similares