Um arcabouço em TLA+ para especificação e verificação de algoritmos distribuídos usando o modelo Heard-Of - Pazin, Yuri de Souza; Dotti, Fernando Luis (Anais do Workshop de Testes e Tolerância a Falhas (WTF); 2025: Anais do XXVI Workshop de Testes e Tolerância a FalhasDO - 10.5753/wtf.2025.9510, 2025)
Algoritmos distribuídos tolerantes a falhas são essenciais em diversos sistemas críticos, tornando sua verificação formal indispensável. O TLA+ tem sido crescentemente adotado para esse fim, apesar dos desafios enfrentados pelos desenvolvedores, como a complexidade inerente ao uso de formalismos e a escolha do nível de abstração adequado: modelos muito complexos sofrem com a explosão do espaço de estados, enquanto modelos simplificados podem comprometer a validade da verificação formal. O modelo Heard-of é uma abstração importante para a especificação e verificação de algoritmos distribuídos baseados em rodadas, permitindo tanto o raciocínio integrado sobre sincronia e falhas quanto mitigar a explosão do espaço de estados. O modelo Heard-of representa os conjuntos de mensagens que chegam a cada processo em uma rodada, e não a ordem entre elas, levando a uma importante redução no espaço de estados. Dada a importância de TLA+ e do modelo Heard-of, neste artigo propomos um framework que provê as abstrações principais do modelo Heard-of em TLA+. Este framework é exemplificado e avaliado com base no algoritmo de Uniform Voting, para o qual também são discutidas propriedades e suas verificações por model checking avaliando o espaço de estados construido e tempo necessários para tal.