Verificación utilizando Dynamite de la corrección del modelo Chord

"La herramienta Dynamite permite traducir modelos formales realizados en el lenguaje de modelado Alloy en teorías del demostrador semiautomático PVS, pero no fue probado con modelos tan complejos como un modelo completo del protocolo Chord. El objetivo inicial de este trabajo fue demostrar la c...

Descripción completa

Detalles Bibliográficos
Autores principales: Dantur, Juan Pablo, Ocamica, Santiago
Otros Autores: Frías, Marcelo
Formato: Proyecto final de Grado
Lenguaje:Español
Publicado: 2019
Materias:
DYNAMITE
SOFTWARE
VERIFICACION DE SOFTWARE
Acceso en línea:http://ri.itba.edu.ar/handle/123456789/1786
Aporte de:
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) de Instituto Tecnológico de Buenos Aires (ITBA)
id I32-R138-123456789-1786
record_format dspace
spelling I32-R138-123456789-17862022-12-07T14:34:23Z Verificación utilizando Dynamite de la corrección del modelo Chord Dantur, Juan Pablo Ocamica, Santiago Frías, Marcelo Moscato, Mariano DYNAMITE SOFTWARE VERIFICACION DE SOFTWARE "La herramienta Dynamite permite traducir modelos formales realizados en el lenguaje de modelado Alloy en teorías del demostrador semiautomático PVS, pero no fue probado con modelos tan complejos como un modelo completo del protocolo Chord. El objetivo inicial de este trabajo fue demostrar la correctitud del protocolo Chord utilizando Dynamite. Durante el desarrollo del Proyecto Final nos encontramos con limitaciones relacionadas a la traducción de Alloy a PVS por parte de Dynamite. Por este motivo, el objetivo del trabajo pasó a ser el de probar Dynamite con el modelo de Chord mencionado anteriormente y de esta forma evaluar la aplicabilidad de Dynamite para este objetivo. Se pudo contribuir al avance de Dynamite a través del reporte de problemas relacionados a la traducción del modelo de Alloy de Chord. También quedaron demostrados con Dynamite todos los lemas sobre los espacios de identificadores y dos de los cinco teoremas principales sobre la correctitud de Chord dado que su invariante se cumple." Proyecto final Ingeniería Informática (grado) - Instituto Tecnológico de Buenos Aires, Buenos Aires, 2019 2019-10-03T18:05:22Z 2019-10-03T18:05:22Z 2019-08-12 Proyecto final de Grado http://ri.itba.edu.ar/handle/123456789/1786 es application/pdf
institution Instituto Tecnológico de Buenos Aires (ITBA)
institution_str I-32
repository_str R-138
collection Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA)
language Español
topic DYNAMITE
SOFTWARE
VERIFICACION DE SOFTWARE
spellingShingle DYNAMITE
SOFTWARE
VERIFICACION DE SOFTWARE
Dantur, Juan Pablo
Ocamica, Santiago
Verificación utilizando Dynamite de la corrección del modelo Chord
topic_facet DYNAMITE
SOFTWARE
VERIFICACION DE SOFTWARE
description "La herramienta Dynamite permite traducir modelos formales realizados en el lenguaje de modelado Alloy en teorías del demostrador semiautomático PVS, pero no fue probado con modelos tan complejos como un modelo completo del protocolo Chord. El objetivo inicial de este trabajo fue demostrar la correctitud del protocolo Chord utilizando Dynamite. Durante el desarrollo del Proyecto Final nos encontramos con limitaciones relacionadas a la traducción de Alloy a PVS por parte de Dynamite. Por este motivo, el objetivo del trabajo pasó a ser el de probar Dynamite con el modelo de Chord mencionado anteriormente y de esta forma evaluar la aplicabilidad de Dynamite para este objetivo. Se pudo contribuir al avance de Dynamite a través del reporte de problemas relacionados a la traducción del modelo de Alloy de Chord. También quedaron demostrados con Dynamite todos los lemas sobre los espacios de identificadores y dos de los cinco teoremas principales sobre la correctitud de Chord dado que su invariante se cumple."
author2 Frías, Marcelo
author_facet Frías, Marcelo
Dantur, Juan Pablo
Ocamica, Santiago
format Proyecto final de Grado
author Dantur, Juan Pablo
Ocamica, Santiago
author_sort Dantur, Juan Pablo
title Verificación utilizando Dynamite de la corrección del modelo Chord
title_short Verificación utilizando Dynamite de la corrección del modelo Chord
title_full Verificación utilizando Dynamite de la corrección del modelo Chord
title_fullStr Verificación utilizando Dynamite de la corrección del modelo Chord
title_full_unstemmed Verificación utilizando Dynamite de la corrección del modelo Chord
title_sort verificación utilizando dynamite de la corrección del modelo chord
publishDate 2019
url http://ri.itba.edu.ar/handle/123456789/1786
work_keys_str_mv AT danturjuanpablo verificacionutilizandodynamitedelacorrecciondelmodelochord
AT ocamicasantiago verificacionutilizandodynamitedelacorrecciondelmodelochord
_version_ 1765660816307126272

Ejemplares similares