Um arcabouço em TLA+ para especificação e verificação de algoritmos distribuídos usando o modelo Heard-Of

• Yuri de Souza Pazin PUCRS
• Fernando Luis Dotti PUCRS https://orcid.org/0000-0001-9061-4695

DOI: https://doi.org/10.5753/wtf.2025.9510

Resumo

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.

Palavras-chave: Algoritmos Distribuídos, Modelagem para Tolerância a Falhas, Tolerância a Falhas, Validação Experimental e Simulação

Referências

Agência Nacional de Vigilância Sanitária (ANVISA) (2020). Guia para Validação de Sistemas Computadorizados - Guia nº 33/2020. Agência Nacional de Vigilância Sanitária.

Barbosa, R., Fonseca, A., and Araujo, F. (2021). Reductions and abstractions for formal verification of distributed round-based algorithms. Software Quality Journal, 29(3): 705–731.

Biely, M., Widder, J., Charron-Bost, B., Gaillard, A., Hutle, M., and Schiper, A. (2007). Tolerating corrupted communication. In Proceedings of the twenty-sixth annual ACM symposium on Principles of distributed computing, pages 244–253.

Bögli, R., Lerena, L., Tsigkanos, C., and Kehrer, T. (2025). A systematic literature review on a decade of industrial TLA+ practice. In International Conference on Integrated Formal Methods, pages 24–34. Springer.

Castro, M., Liskov, B., et al. (1999). Practical Byzantine fault tolerance. In OSDI, volume 99, pages 173–186.

Chaouch-Saad, M., Charron-Bost, B., and Merz, S. (2009). A reduction theorem for the verification of round-based distributed algorithms. In International Workshop on Reachability Problems, pages 93–106. Springer.

Charron-Bost, B. and Schiper, A. (2009). The Heard-Of model: computing in distributed systems with benign faults. Distributed Computing, 22(1): 49–71.

Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., and Tacchella, A. (2002). NuSMV 2: An open-source tool for symbolic model checking. In Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27–31, 2002 Proceedings 14, pages 359–364. Springer.

Hutle, M. and Schiper, A. (2007). Communication predicates: A high-level abstraction for coping with transient and dynamic faults. In 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN’07), pages 92–101. IEEE.

Lamport, L. (2002). Specifying systems: The TLA+ language and tools for hardware and software engineers.

Lamport, L., Shostak, R. E., and Pease, M. C. (1982). The Byzantine generals problem. ACM Transactions on Programming Languages and Systems, 4: 382–401.

Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., and Deardeuff, M. (2014). Use of formal methods at amazon web services. See [link], page 16.

RTCA (2011). DO-178C: Software Considerations in Airborne Systems and Equipment Certification. Supersedes DO-178B (1992).

Tsuchiya, T. and Schiper, A. (2007). Model checking of consensus algorithms. In 2007 26th IEEE International Symposium on Reliable Distributed Systems (SRDS 2007), pages 137–148. IEEE.

Van Steen, M. (2002). Distributed systems principles and paradigms. Network, 2(28): 1.

Zhai, S., Li, X., and Ge, N. (2023). HOME: Heard-Of based formal modeling and verification environment for consensus protocols. In 2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), pages 16–20. IEEE.