Registro:
| Documento: | Tesis de Grado |
| Título: | Verificación de correctitud para tipos de datos replicados en Coq |
| Autor: | Gómez, Pablo Nicolás |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2023-09-12 |
| Fecha de defensa: | 2021-06-10 |
| Fecha en portada: | 2021 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Roldán, Christian Hugo |
| Director Asistente: | Melgratti, Hernán Claudio |
| Idioma: | Español |
| Palabras clave: | REPLICACION; TIPOS DE DATOS REPLICADOS; CORRECTITUD DE IMPLEMENTACIONES; SIMULACIONCOQ |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000484_Gomez |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000484_Gomez.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000484_Gomez |
| Ubicación: | Dep.COM 000484 |
| 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. Gómez, Pablo Nicolás. (2021). Verificación de correctitud para tipos de datos replicados en Coq. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000484_Gomez |
Resumen:
La replicación de datos es un concepto fundamental en sistemas distribuidos ya que ofrece garantías como escalabilidad y alta disponibilidad a expensas de tener una visión inconsistente del estado del sistema. Esto significa que los usuarios de dicho sistema, temporalmente, podrían percibir diferencias sobre el estado del mismo. En particular, esta tesis se concentra en un enfoque de replicación basada en estados, donde cada réplica (o nodo) que compone al sistema, transmite su estado al resto de las réplicas con el fin de que estas puedan combinarlo con su propio estado y alcancen así un mismo estado común. La literatura propone los tipos de datos replicados o RDTs (por su acrónimo en inglés, Replicated Data Types), quienes lidean con inconsistencias temporales que puedan existir y resuelven de forma automática cuando existen conflictos entre escrituras concurrentes. Diferentes líneas de investigación han abordado el problema de especificar e implementar RDTs. Más aún, hay demostraciones manuales sobre la correcta implementación de un RDT con respecto a su especificación. En esta tesis proponemos abordar el problema de formalizar y verificar la correcta implementación de RDTs utilizando el asistente de demostraciones Coq. Coq es un sistema formal de semidecisión de manejo de demostraciones de teoremas chequeadas por computadora. Proveemos por lo tanto, de un marco de trabajo para verificar la correctitud de RDTs de una manera computarizada, lo cual ofrece una alternativa confiable y mecánica de abordar esta tarea. Más concretamente, en esta tesis nos centramos en realizar la experiencia de formalizar en Coq una especificación y una implementación de un RDT (tomando como caso de estudio el tipo de datos: Contador ). Para esto, (i) mostraremos cómo transformar las definiciones existentes en definiciones equivalentes en Coq. Luego, (ii) probaremos que la implementación del tipo de datos es correcta, basándonos en un resultado que establece la existencia de una relación de simulación entre la semántica operacional asociada a la especificación, y la implementación concreta del Contador. Finalmente, (iii) presentamos una prueba en el asistente sobre la correcta implementación del tipo de datos, mostrando para esto, la existencia de dicha relación de simulación.
Citación:
---------- APA ----------
Gómez, Pablo Nicolás. (2021). Verificación de correctitud para tipos de datos replicados en Coq. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000484_Gomez
---------- CHICAGO ----------
Gómez, Pablo Nicolás. "Verificación de correctitud para tipos de datos replicados en Coq". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2021.https://hdl.handle.net/20.500.12110/seminario_nCOM000484_Gomez
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000484_Gomez.pdf
Distrubución geográfica
