Please use this identifier to cite or link to this item: https://hdl.handle.net/1822/84345

Full metadata record
DC FieldValueLanguage
dc.contributor.advisorCunha, Alcinopor
dc.contributor.authorSoares, Cecília da Conceição de Oliveirapor
dc.date.accessioned2023-05-09T09:55:16Z-
dc.date.available2023-05-09T09:55:16Z-
dc.date.issued2022-
dc.date.submitted2022-
dc.identifier.urihttps://hdl.handle.net/1822/84345-
dc.descriptionDissertação de mestrado integrado em Informatics Engineeringpor
dc.description.abstractO protocolo de máquinas de estado replicadas (MER) é uma peça fundamental dos sistemas distribuídos. No centro deste protocolo estão os algoritmos de consenso, como o Paxos, usados para manter a consistência das MER. Todavia, os sistemas modernos não podem depender estritamente das técnicas de MER, estes devem também implementar estratégias de reconfiguração. Estas estratégias consistem em alterar a configuração do sistema, adicionando, removendo ou substituindo os processos que o compõem. Dada a sua complexidade, a implementação de protocolos de reconfiguração é muito suscetível a erros, daí que seja aconselhável a especificação, validação e verificação dos mesmos. No presente trabalho apresentamos uma especificação em linguagem Alloy do protocolo de reconfiguração Vertical Paxos e do protocolo de consenso Paxos. Além destes, modelamos o protocolo Multi-Paxos, o qual implementa uma MER. Estes protocolos estão intrinsecamente relacionados e a compreensão do primeiro é facilitada com o conhecimento dos demais. Atualmente, o Alloy é uma das linguagens de especificação mais populares, mas pouco explorada na modelação de algoritmos distribuídos e, tanto quanto sabemos, não existe ainda nenhuma especificação dos referidos protocolos em Alloy. O presente trabalho visa modelar e validar os referidos protocolos, bem como verificar as suas propriedades de safety, de modo a obtermos confiança nas especificações. Ademais, realizamos uma avaliação de desempenho de diferentes solvers e estratégias de decomposição nativas do Alloy, bem como uma breve análise comparativa com o TLA+.por
dc.description.abstractState machine replication (SMR) protocols have a crucial role in distributed systems. At the heart of these protocols are the consensus algorithm, such as Paxos, responsible for SMR’s consistency. However, modern systems cannot only rely on SMR thecniques, they must implement reconfiguration strategies, which consist in changing their configurations by adding, removing or replacing their processes. Due to its complexity, implementing a reconfiguration algorithm is error-prone, therefore its specification, validation and verification is advisable. In this work, we present a specification, in Alloy, of the reconfiguration protocol Vertical Paxos and the consensus protocol Paxos. Besides, we model the Multi-Paxos protocol which implements a SMR. These three protocols are intrinsically related and, once we are familiar with Paxos and Multi-Paxos, understanding Vertical Paxos becomes straigthfoward. Nowadays, Alloy is one of the most popular specification languages, but littleexplored in modeling and analyzing distributed algorithms. As far as we know, there is still no specification of these protocols in Alloy. The aim of this work is to model and validate these protocols, as well as to verify their safety properties, in order to obtain confidence in our specifications. Furthermore, we evaluate the performance of different solvers and decomposition strategies. Finally, we carry out a brief comparative analysis with TLA+.por
dc.language.isoporpor
dc.rightsopenAccesspor
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/por
dc.subjectAlloypor
dc.subjectMERpor
dc.subjectMulti-Paxospor
dc.subjectPaxospor
dc.subjectVertical Paxospor
dc.subjectSMRpor
dc.titleFormalização da reconfiguração de protocolos de consenso usando Alloypor
dc.typemasterThesiseng
dc.identifier.tid203261216por
thesis.degree.grantorUniversidade do Minhopor
sdum.degree.grade18 valorespor
sdum.uoeiEscola de Engenhariapor
dc.subject.fosEngenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informáticapor
Appears in Collections:BUM - Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
Cecília-Conceição-Soares-dissertação-final.pdf6,81 MBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID