Specifying software provides safety guarantees for the system and facilitates modifications and optimizations on the specified program, which is specially interesting for concurrent or distributed systems, where there are many behaviors to be considered. Specifications for this systems can be written in the specification language TLA+, which is composed by definitions close to mathematics and tools that allow verification of temporal logic described properties. This work proposes an automatic translator of TLA+ specifications to the functional and concurrent programming language Elixir, allowing the execution of the specified system.
Especificar software traz garantias de segurança para o sistema e facilita modificações e otimizações sobre o programa especificado, o que é especialmente interessante para sistemas concorrentes ou distribuídos, onde há muitos comportamentos a se considerar. Especificações para esses sistemas podem ser escritas com a linguagem de especificação \TLAA, que é composta por definições próximas à matemática e ferramentas que permitem a verificação de propriedades descritas em lógica temporal. Este trabalho propõe um tradutor automático de especificações em \TLA para a linguagem de programação funcional e concorrente Elixir, permitindo a execução do sistema especificado.