Registro:
| Documento: | Tesis de Grado |
| Disciplina: | computacion |
| Título: | ParAlloy una implementación paralelay distribuida para DynAlloy |
| Autor: | Rosner, Nicolás |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2024-08-30 |
| Fecha de defensa: | 2006 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Frias, Marcelo Fabián; López Pombo, Carlos Gustavo |
| Idioma: | Español |
| Palabras clave: | ALLOY; DYNALLOY; PARALLOY; VERIFICACION DE PROPIEDADES; DEMOSTRACION (SEMI) AUTOMATICA DE TEOREMAS; METODOS FORMALES (RELACIONALES); SISTEMAS DISTRIBUIDOS; PROGRAMACION PARALELA; JINI; JAVASPACES |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000302_Rosner |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000302_Rosner.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000302_Rosner |
| Ubicación: | Dep.COM 000302 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Rosner, Nicolás. (2006). ParAlloy una implementación paralelay distribuida para DynAlloy. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000302_Rosner |
Resumen:
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.
Citación:
---------- APA ----------
Rosner, Nicolás. (2006). ParAlloy una implementación paralelay distribuida para DynAlloy. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000302_Rosner
---------- CHICAGO ----------
Rosner, Nicolás. "ParAlloy una implementación paralelay distribuida para DynAlloy". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2006.https://hdl.handle.net/20.500.12110/seminario_nCOM000302_Rosner
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000302_Rosner.pdf
Distrubución geográfica
