Defesa de Dissertação de Caio Serra de Mello, 04/07/25, 14h, na sala 321 do Instituto de Computação
Formal Modeling and Verification of the XMPP Protocol Using UPPAAL
Resumo:
Esta dissertação apresenta uma verificação formal abrangente do Extensible Messaging and Presence Protocol (XMPP) utilizando o verificador de modelos UPPAAL. Demonstramos como autômatos temporizados podem ser empregados de forma eficaz para modelar e verificar propriedades críticas do XMPP, com foco em propriedades de liveness. A pesquisa explora os fundamentos teóricos dos timed automata e do protocolo XMPP, e então aplica esses conceitos para desenvolver um modelo formal que captura o comportamento essencial dos componentes XMPP, incluindo clientes, servidores e os canais de comunicação entre eles. Verificamos propriedades como: Garantias de entrega de mensagens, ausência de deadlocks, tratamento adequado do estabelecimento e término de streams. Nossa abordagem combina análise teórica rigorosa com implementação prática, fornecendo uma metodologia que pode ser aplicada para verificar diferentes protocolos de comunicação em tempo real em vários domínios. Os resultados mostram que a verificação formal utilizando o UPPAAL pode identificar eficazmente potenciais problemas em implementações XMPP e garantir propriedades essenciais, aumentando substancialmente a confiança em sua correção e confiabilidade.
Abstract:
This dissertation presents a comprehensive formal verification of the Extensible Messaging and Presence Protocol (XMPP) using the UPPAAL model checker. We demonstrate how timed automata can be effectively employed to model and verify critical XMPP properties, focusing on liveness properties. The research explores the theoretical foundations of timed automata and the XMPP protocol, and then applies these concepts to develop a formal model that captures the essential behavior of XMPP components, including clients, servers, and the communication channels between them. We verify properties such as message delivery guarantees, absence of deadlocks, and proper handling of stream establishment and termination. Our approach combines rigorous theoretical analysis with practical implementation, providing a methodology that can be applied to verify different real-time communication protocols across various domains. The results show that formal verification using UPPAAL can effectively identify potential issues in XMPP implementations and ensure essential properties, substantially increasing confidence in their correctness and reliability.
Banca examinadora:
Prof. Bruno Lopes Vieira, UFF – Presidente
Prof. Mario Roberto Folhadela Benevides, UFF
Prof. Edward Hermann Haeusler, PUC-Rio