Fully-Tested code generation from TLA+ specifications

  • Gabriela Moreira UDESC
  • Cristiano Vasconcellos UDESC
  • Janine Kniess UDESC


Specifying software systems brings value by increasing confidence. However, engineers struggle to adopt this practice for its steep learning curve and lack of connection to production software. These problems can be addressed with simulation of specifications and generation of test cases. TLA+ (Temporal Logic of Actions+), a specification language used by big tech companies, is still mostly devoid of this tooling. This work proposes a combination of code and test generation from TLA+ files with the goal of making specification writers obtain value from their specifications as soon as possible.

Palavras-chave: TLA, Elixir, Model-Based testing, Code generation, Test generation, Formal specification
Como Citar

Selecione um Formato
MOREIRA, Gabriela; VASCONCELLOS, Cristiano; KNIESS, Janine. Fully-Tested code generation from TLA+ specifications. In: SIMPÓSIO BRASILEIRO DE TESTES DE SOFTWARE SISTEMÁTICO E AUTOMATIZADO (SAST), 7. , 2022, Uberlândia. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2022 . p. 19–28.