Verificación de correctitud para tipos de datos replicados en Coq

Mostrar todas las versiones(3)

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 diferenc...

Descripción completa

Detalles Bibliográficos
Autor principal: Gómez, Pablo Nicolás
Otros Autores: Roldán, Christian Hugo
Formato: Tesis de grado publishedVersion
Lenguaje:Español
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2021
Materias:
REPLICACION
TIPOS DE DATOS REPLICADOS
CORRECTITUD DE IMPLEMENTACIONES
SIMULACION
COQ
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000484_Gomez
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id seminario:seminario_nCOM000484_Gomez
record_format dspace
spelling seminario:seminario_nCOM000484_Gomez2025-05-09T18:45:34Z Verificación de correctitud para tipos de datos replicados en Coq Gómez, Pablo Nicolás Roldán, Christian Hugo Melgratti, Hernán Claudio REPLICACION TIPOS DE DATOS REPLICADOS CORRECTITUD DE IMPLEMENTACIONES SIMULACION COQ 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. Fil: Gómez, Pablo Nicolás. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2021-06-10 info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion application/pdf spa info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000484_Gomez
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Español
orig_language_str_mv spa
topic REPLICACION
TIPOS DE DATOS REPLICADOS
CORRECTITUD DE IMPLEMENTACIONES
SIMULACION
COQ
spellingShingle REPLICACION
TIPOS DE DATOS REPLICADOS
CORRECTITUD DE IMPLEMENTACIONES
SIMULACION
COQ
Gómez, Pablo Nicolás
Verificación de correctitud para tipos de datos replicados en Coq
topic_facet REPLICACION
TIPOS DE DATOS REPLICADOS
CORRECTITUD DE IMPLEMENTACIONES
SIMULACION
COQ
description 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.
author2 Roldán, Christian Hugo
author_facet Roldán, Christian Hugo
Gómez, Pablo Nicolás
format Tesis de grado
Tesis de grado
publishedVersion
author Gómez, Pablo Nicolás
author_sort Gómez, Pablo Nicolás
title Verificación de correctitud para tipos de datos replicados en Coq
title_short Verificación de correctitud para tipos de datos replicados en Coq
title_full Verificación de correctitud para tipos de datos replicados en Coq
title_fullStr Verificación de correctitud para tipos de datos replicados en Coq
title_full_unstemmed Verificación de correctitud para tipos de datos replicados en Coq
title_sort verificación de correctitud para tipos de datos replicados en coq
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2021
url https://hdl.handle.net/20.500.12110/seminario_nCOM000484_Gomez
work_keys_str_mv AT gomezpablonicolas verificaciondecorrectitudparatiposdedatosreplicadosencoq
_version_ 1831983611663876096

Ejemplares similares