Defesa de Dissertação de Mestrado de Camila de Souza Ferreira, 24/11/25, 14h, por videoconferência
Link para defesa: https://meet.google.com/krg-awyy-shu
Modelagem do Consenso Bizantino em Timed Automata
Resumo:
Esta dissertação apresenta uma modelagem formal para o Consenso Bizantino, problema clássico de sistemas distribuídos formalizado por Leslie Lamport, Robert Shostak e Marshall Pease. O estudo aborda a necessidade de múltiplos agentes alcançarem um acordo confiável, mesmo na presença de falhas ou informações conflitantes. A resolução deste problema é essencial para garantir a consistência e a segurança em aplicações críticas, como blockchains e serviços de replicação de dados, assegurando que os processos corretos cheguem a uma decisão comum. Para a modelagem do algoritmo, foi empregada a técnica de verificação de modelos (model checking) com o uso da ferramenta UPPAAL. A metodologia se baseia na utilização de autômatos temporizados (timed automata), uma extensão dos autômatos finitos que permite modelar o comportamento temporal de sistemas de tempo real. Especificamente, o trabalho foca na modelagem da solução por mensagens orais, uma das abordagens clássicas para o Problema dos Generais Bizantinos. O modelo desenvolvido no UPPAAL representa a comunicação entre os generais, a propagação de ordens e o processo de decisão majoritária, considerando a presença de agentes leais e traidores. O modelo também permite parametrizar o número de generais e de traidores, possibilitando a simulação de diferentes cenários e a verificação de propriedades fundamentais do protocolo. Por meio desta abordagem, busca-se demonstrar a viabilidade da verificação formal para garantir que requisitos críticos, como a concordância entre os agentes honestos, sejam cumpridos, contribuindo para a concepção de sistemas distribuídos mais seguros e confiáveis.
Abstract:
This dissertation presents a formal modeling for the Byzantine Consensus, a classic problem in distributed systems formalized by Leslie Lamport, Robert Shostak, and Marshall Pease. The study addresses the need for multiple agents to reach a reliable agreement, even in the presence of failures or conflicting information. The resolution of this problem is essential to ensure consistency and security in critical applications, such as blockchains and data replication services, by guaranteeing that correct processes arrive at a common decision. For modeling the algorithm, the model checking technique was employed using the UPPAAL tool. The methodology is based on the use of timed automata, an extension of finite automata that allows for the modeling of the temporal behavior of real-time systems. Specifically, the work focuses on modeling the solution with oral messages, one of the classic approaches to the Byzantine Generals Problem. The model developed in UPPAAL represents the communication between generals, the propagation of orders, and the majority decision-making process, considering the presence of loyal and traitorous agents. The proposed model also allows the parameterization of the number of generals and traitors, enabling the simulation of different scenarios and the verification of the protocol’s fundamental properties. Through this approach, the aim is to demonstrate the feasibility of formal verification to ensure that critical requirements, such as agreement among honest agents, are met, thereby contributing to the design of safer and more reliable distributed systems.
Banca examinadora:
Prof. Bruno Lopes Vieira, UFF – Presidente
Prof. Igor Machado Coelho, UFF
Prof. Edward Hermann Haeusler, PUC-Rio