A eSpark usou TLA+ para provar que nenhum design atendia às 3 regras e então abriu mão de uma delas

A eSpark Learning, fornecedora de tecnologia educacional para escolas de ensino fundamental, executava um processo manual e semirregular de configuração para cada cliente, que coordenava vários sistemas de terceiros e modificava diretamente as redes de TI dos clientes. À medida que a base de usuários crescia, a carga de trabalho se tornou insustentável — a equipe de suporte percebeu que precisaria de uma nova contratação em tempo integral a cada ano só para acompanhar. A liderança sempre considerou a automação do processo perigosa demais: um erro poderia afetar a rede de um cliente e custar o contrato.

O engenheiro Hillel Wayne havia usado recentemente especificação formal (no estilo TLA+) em um projeto de upload em lote e reduzido uma semana do prazo de entrega ao detectar bugs de arquitetura antes de escrever código. O gerente de projeto havia definido três propriedades que a substituição automatizada precisava garantir para ser segura. Wayne modelou o sistema em uma linguagem de especificação e o executou por meio de um verificador de modelos, que simula exaustivamente todos os cenários que uma especificação permite e retorna um traço concreto quando encontra um que viola uma regra.

Após dois dias de modelagem, todo design ou falhava imediatamente ou continha uma falha sutil que poderia passar despercebida em produção por meses antes de colapsar. Alguns designs satisfaziam duas das três propriedades exigidas, mas nenhum satisfazia todas as três. Em vez de escolher um de qualquer forma e torcer para dar certo, Wayne trouxe o gerente de projeto para os artefatos de modelagem, mostrou concretamente como cada design falharia e perguntou de qual propriedade o negócio poderia abrir mão.

Especialistas internos em design determinaram que uma propriedade só precisava valer usualmente, não sempre. Com essa única concessão delimitada, o verificador de modelos confirmou que vários designs agora funcionariam, e a equipe construiu um deles. O serviço automatizado de configuração operou sem incidentes por anos depois disso, sobrevivendo ao tempo de casa dos engenheiros que o construíram.

O verificador de modelos provou que nenhum design atendia às 3 regras, o que levou à negociação de um requisito.

Modelar em uma linguagem de especificação é barato de descartar; uma base de código quase pronta não é, então testar cada ideia de design antes da implementação evitou tempo de engenharia desperdiçado.

Um verificador de modelos retorna um traço de falha concreto, que é mais persuasivo para uma parte interessada não engenheira do que um aviso abstrato de risco.

Trazer à tona "nenhum desses designs satisfaz todos os três requisitos" antes de escrever código transformou uma suposição implícita e não examinada em uma decisão explícita que o gerente de projeto podia de fato tomar.

Quando todo design que você tenta parece falhar, modele o espaço formalmente primeiro. Um verificador de modelos transforma uma vaga sensação de risco em uma concessão específica e negociável que você pode levantar antes de qualquer código ser escrito.

O serviço automatizado de gestão de configuração operou com eficiência por anos, bem além do tempo de casa dos engenheiros que o construíram. Wayne passou a trabalhar em tempo integral como consultor de especificação formal e a escrever sobre a prática, incluindo um livro sobre o assunto e trabalho de documentação para a linguagem de especificação Alloy.