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

Dantur, Juan Pablo; Ocamica, Santiago

proyecto final de grado.page.titleprefix
Verificación utilizando Dynamite de la corrección del modelo Chord

dc.contributor.advisor	Frías, Marcelo
dc.contributor.advisor	Moscato, Mariano
dc.contributor.author	Dantur, Juan Pablo
dc.contributor.author	Ocamica, Santiago
dc.date.accessioned	2019-10-03T18:05:22Z
dc.date.available	2019-10-03T18:05:22Z
dc.date.issued	2019-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.notes	Proyecto final Ingeniería Informática (grado) - Instituto Tecnológico de Buenos Aires, Buenos Aires, 2019	es
dc.identifier.uri	http://ri.itba.edu.ar/handle/123456789/1786
dc.language.iso	es	es
dc.subject	DYNAMITE	es
dc.subject	SOFTWARE	es
dc.subject	VERIFICACION DE SOFTWARE	es
dc.title	Verificación utilizando Dynamite de la corrección del modelo Chord	es
dc.type	Proyecto final de Grado	es
dspace.entity.type	Proyecto final de Grado
itba.description.filiation	Fil: Dantur, Juan Pablo. Instituto Tecnológico de Buenos Aires; Argentina.
itba.description.filiation	Fil: Ocamica, Santiago. Instituto Tecnológico de Buenos Aires; Argentina.