Notas do vídeo Introduction to TLA+, de Leslie Lamport.
O que é TLA+?
Uma linguagem para modelar, em alto nível, as partes críticas de sistemas digitais. Foi criada para sistemas concorrentes e distribuídos e pode ajudar a encontrar erros de projeto antes de escrever código.
Suas ferramentas incluem:
- TLC: o verificador de modelos.
- TLAPS: o sistema de provas de TLA+.
- TLA+ Toolbox: uma IDE para escrever especificações e executar as ferramentas.
A principal lição para mim é abstração: aprender a focar nas partes de um sistema que importam para entender seu comportamento.
Em tradução livre:
A parte difícil de aprender a escrever especificações TLA+ é aprender a pensar de forma abstrata sobre o sistema.
— Brannon Batson, citado no vídeo
Máquinas de estados
- Um estado é uma atribuição de valores a variáveis.
- Um comportamento é uma sequência de estados.
- Uma máquina de estados especifica os possíveis estados iniciais e quais estados podem suceder um determinado estado.
O objetivo é verificar se o sistema satisfaz as propriedades exigidas em todos os comportamentos permitidos.
Mais material
- The TLA+ Video Course, de Leslie Lamport.
- How Amazon Web Services Uses Formal Methods, sobre como a AWS adotou TLA+.
- TLA+ Foundation.
- Organização TLA+ no GitHub.