Loading...
Verificación utilizando Dynamite de la corrección del modelo Chord
Dantur, Juan Pablo Ocamica, Santiago
Dantur, Juan Pablo
Ocamica, Santiago
Type
Proyecto final de grado
Citations
Altmetric:
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."
Description
Date
2019-08-12
Journal Title
Journal ISSN
Volume Title
Publisher
Collections
Files
Loading...
Proyecto_Final_Dantur
Adobe PDF, 425.36 KB
Research Projects
Organizational Units
Journal Issue
Keywords
DYNAMITE, SOFTWARE, VERIFICACION DE SOFTWARE