Fully-Tested code generation from TLA+ specifications - Moreira, Gabriela; Vasconcellos, Cristiano; Kniess, Janine (Anais do Simpósio Brasileiro de Testes de Software Sistemático e Automatizado (SAST); 2022: Anais do VII Simpósio Brasileiro de Testes de Software Sistemático e Automatizado, 2022)
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.