Verificación formal de protocolos distribuidos

Mostrar todas las versiones(2)

Tesis (Lic. en Cs de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019.

Guardado en:
Detalles Bibliográficos
Autor principal: Naser Pastoriza, Alejandro José
Otros Autores: D'Argenio, Pedro Ruben
Formato: bachelorThesis publishedVersion
Lenguaje:Español
Publicado: 2020
Materias:
Teoría de la computación
Modelos computacionales
Protocolos distribuídos
Distributed computing models
Distributed algorithms
Theory of computation
Paxos
Atomic broadcast
Formal verification
Distributed protocols
Acceso en línea:http://hdl.handle.net/11086/15004
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-15004
record_format dspace
spelling I10-R141-11086-150042023-08-31T13:19:19Z Verificación formal de protocolos distribuidos Naser Pastoriza, Alejandro José D'Argenio, Pedro Ruben Gotsman, Alexey Teoría de la computación Modelos computacionales Protocolos distribuídos Distributed computing models Distributed algorithms Theory of computation Paxos Atomic broadcast Formal verification Distributed protocols Tesis (Lic. en Cs de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019. Fil: Naser Pastoriza, Alejandro José. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. En esta tesis probamos la correctitud de tres protocolos distribuidos. Primero, el algoritmo Single Decree Paxos que resuelve el problema de llegar a un acuerdo, o alcanzar consenso, entre un conjunto de procesos. Segundo, una optimización del protocolo de broadcast atómico de ZooKeeper que implementa un esquema primary-backup en el cual un proceso primario ejecuta las operaciones del cliente y utliza Zab para propagar los correspondientes cambios incrementales de estado a los procesos backup. Dicha optimización desarrollada por Alexey Gotsman, Joe Izraelevitz y Gregory Chockler, reduce la transferencia de estado durante la elección del lı́der. Por último, una variante del protocolo Vertical Paxos en las lı́neas de Reconfigurable Atomic Transaction Commit, Bravo & Gotsman, PODC’19, una clase de algoritmo Paxos en el cual reconfiguraciones pueden ocurrir durante el proceso de alcanzar acuerdo. Posteriormente, formalizamos la prueba de Single Decree Paxos en Dafny, un lenguaje de programación verifier-friendly basado en lógica de Floyd-Hoare que automatiza la verificación a través del SMT solver Z3. In this thesis we prove the correctness of three distributed protocols. First, the Single Decree Paxos algorithm which solves the problem of reaching agreement, or consensus, among a set of processes. Secondly, an optimization of the ZooKeeper atomic broadcast protocol which implements a primary-backup scheme in which a primary process executes client operations and uses Zab to propagate the corresponding incremental state changes to the backup processes. Such optimization developed by Alexey Gotsman, Joe Izraelevitz and Gregory Chockler, reduces state transfer during the leader election. Lastly, a variant of Vertical Paxos along the lines of Reconfigurable Atomic Transaction Commit, Bravo & Gotsman, PODC’19, a class of Paxos algorithm in which reconfigurations can occur in the middle of reaching agreement. Finally, we formalize the proof of Single Decree Paxos in Dafny, a verifier-friendly programming language based on Floyd-Hoare logic that automates verification via the Z3 SMT solver. Fil: Naser Pastoriza, Alejandro José. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2020-03-06T20:40:38Z 2020-03-06T20:40:38Z 2019 bachelorThesis info:eu-repo/semantics/publishedVersion http://hdl.handle.net/11086/15004 spa Attribution-NonCommercial-NoDerivatives 4.0 Internacional http://creativecommons.org/licenses/by-nc-nd/4.0/
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Español
topic Teoría de la computación
Modelos computacionales
Protocolos distribuídos
Distributed computing models
Distributed algorithms
Theory of computation
Paxos
Atomic broadcast
Formal verification
Distributed protocols
spellingShingle Teoría de la computación
Modelos computacionales
Protocolos distribuídos
Distributed computing models
Distributed algorithms
Theory of computation
Paxos
Atomic broadcast
Formal verification
Distributed protocols
Naser Pastoriza, Alejandro José
Verificación formal de protocolos distribuidos
topic_facet Teoría de la computación
Modelos computacionales
Protocolos distribuídos
Distributed computing models
Distributed algorithms
Theory of computation
Paxos
Atomic broadcast
Formal verification
Distributed protocols
description Tesis (Lic. en Cs de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019.
author2 D'Argenio, Pedro Ruben
author_facet D'Argenio, Pedro Ruben
Naser Pastoriza, Alejandro José
format bachelorThesis
publishedVersion
author Naser Pastoriza, Alejandro José
author_sort Naser Pastoriza, Alejandro José
title Verificación formal de protocolos distribuidos
title_short Verificación formal de protocolos distribuidos
title_full Verificación formal de protocolos distribuidos
title_fullStr Verificación formal de protocolos distribuidos
title_full_unstemmed Verificación formal de protocolos distribuidos
title_sort verificación formal de protocolos distribuidos
publishDate 2020
url http://hdl.handle.net/11086/15004
work_keys_str_mv AT naserpastorizaalejandrojose verificacionformaldeprotocolosdistribuidos
_version_ 1782014733007716352

Ejemplares similares