Proyecto final de Grado:
Verificación utilizando Dynamite de la corrección del modelo Chord

dc.contributor.advisorFrías, Marcelo
dc.contributor.advisorMoscato, Mariano
dc.contributor.authorDantur, Juan Pablo
dc.contributor.authorOcamica, Santiago
dc.date.accessioned2019-10-03T18:05:22Z
dc.date.available2019-10-03T18:05:22Z
dc.date.issued2019-08-12
dc.description.abstract"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."es
dc.description.notesProyecto final Ingeniería Informática (grado) - Instituto Tecnológico de Buenos Aires, Buenos Aires, 2019es
dc.identifier.urihttp://ri.itba.edu.ar/handle/123456789/1786
dc.language.isoeses
dc.subjectDYNAMITEes
dc.subjectSOFTWAREes
dc.subjectVERIFICACION DE SOFTWAREes
dc.titleVerificación utilizando Dynamite de la corrección del modelo Chordes
dc.typeProyecto final de Gradoes
dspace.entity.typeProyecto final de Grado
itba.description.filiationFil: Dantur, Juan Pablo. Instituto Tecnológico de Buenos Aires; Argentina.
itba.description.filiationFil: Ocamica, Santiago. Instituto Tecnológico de Buenos Aires; Argentina.
Archivos
Bloque original
Mostrando1 - 1 de 1
Miniatura
Nombre:
Informe Proyecto Final.pdf
Tamaño:
425.36 KB
Formato:
Adobe Portable Document Format
Descripción:
Proyecto_Final_Dantur
Bloque de licencias
Mostrando1 - 1 de 1
No hay miniatura disponible
Nombre:
license.txt
Tamaño:
1.6 KB
Formato:
Item-specific license agreed upon to submission
Descripción: