Métodos formais: apenas uma boa prática de engenharia? (2024)
(brooker.co.za)- Em sistemas grandes, distribuídos e críticos de baixo nível, métodos formais devem ser vistos não como uma etapa extra apenas para correção, mas como uma prática de engenharia que reduz tempo e custo
- No software, projeto e implementação se misturam facilmente, então mudanças tardias no projeto logo se transformam em retrabalho de implementação e custo de alterar APIs
- Examinar concretamente comportamento e interfaces antes da implementação pode reduzir densidade de bugs e problemas após produção, além de levar mais rápido ao projeto correto
- Em áreas que mudam rápido ou são difíceis de formalizar, como requisitos de usuário, UI, documentação e lógica de preços, a utilidade de um projeto formal prévio abrangente pode ser menor
- Ferramentas como TLA+ e P também podem ser usadas para revisar otimizações e restrições na fase de projeto, reduzindo trade-offs entre correção e desempenho
Métodos formais como boa prática de engenharia
- Métodos formais são uma parte importante de boas práticas de engenharia de software
- Têm valor especial para engenheiros que lidam com sistemas de grande escala, sistemas distribuídos e sistemas críticos de baixo nível
- O ponto de partida é a ideia de que engenharia, no fim, é a atividade de otimizar tempo e custo
- Desempenho, escalabilidade, sustentabilidade e eficiência também entram nessa conta
- Métodos formais não são baratos nem fáceis, e também não se encaixam bem em todo estilo de desenvolvimento, mas a intuição de que só aumentam o custo nem sempre está correta
Dois caminhos para reduzir custo
- O primeiro é reduzir retrabalho
- Diferentemente de outras áreas da engenharia, no software é fácil que projeto e construção aconteçam ao mesmo tempo
- É possível começar a implementar mesmo sem que o projeto esteja suficientemente avançado
- Essa maleabilidade é uma força do software, mas pode transformar iteração de projeto em iteração de implementação e aumentar o custo
- O segundo é gerenciar o custo da mudança
- Quando um sistema ou API já tem clientes, mudar fica muito mais caro e difícil
- Segundo a Lei de Hyrum, com um número suficiente de usuários de uma API, alguém passará a depender de todo comportamento observável, independentemente do contrato definido
- Isolar o comportamento do sistema por meio de APIs é uma ideia importante da engenharia de software, mas continua existindo o limite de que usuários podem depender até de detalhes de implementação
- É possível reimplementar completamente o sistema por trás de uma API, mas a abstração não elimina por si só o custo da mudança
- Trabalho de projeto formal pode reduzir o custo de retrabalho e fazer com que mudanças de interface sejam tratadas mais cedo, aumentando a velocidade e a eficiência na construção de software
Sistemas em que projeto formal se encaixa bem
- Isso não se aplica da mesma forma a todo software
- Em softwares com muitos requisitos de usuário que evoluem rapidamente ou são difíceis de formalizar, o valor de projeto prévio pode enfraquecer
- UI, websites e implementação de lógica de preços entram nessa categoria
- Nessas áreas, há muito retrabalho contínuo, então o custo de projeto prévio pode ficar alto
- A ideia fundamental do ágil é tocar implementação e levantamento de requisitos em paralelo para reduzir o tempo até o lançamento
- Isso permite concluir a implementação mesmo quando o levantamento de requisitos continua em andamento
- Em muitos casos, esse modo de desenvolvimento paralelo é o ideal ou uma condição necessária para viabilizar o progresso
- Em contrapartida, muitas partes de sistemas grandes, distribuídos e de baixo nível têm requisitos bem compreendidos
- Pelo menos existe uma parcela estática suficientemente grande dos requisitos
- Nesse caso, projeto formal prévio pode reduzir bastante retrabalho e densidade de bugs tanto na implementação quanto depois da produção
- Quanto mais os requisitos se parecem com leis da física, maior o valor do projeto e do projeto formal; quanto mais se aproximam de opinião do usuário, menor esse valor
Limites da documentação e da formalização de requisitos
- Escrever claramente os requisitos do usuário é muito valioso, seja de forma formal ou informal
- Se os requisitos não são escritos, tempo pode ser desperdiçado e as pessoas podem seguir em direções diferentes, gerando atrito
- Formalizar todos os requisitos humanos pode ser difícil ou economicamente inviável
- Requisitos estéticos de UI
- Legibilidade da documentação
- Consistência de nomes de API
- Diferenças de opinião sobre abordagens formais também surgem de visões diferentes sobre o que é uma abordagem formal e de que maneira ela gera valor
- Formas como o UML, que transportam o código para diagramas extensos, podem ter pouco valor se não enfrentarem diretamente as perguntas difíceis
- Mesmo um trabalho valioso pode se tornar inútil quando feito com método ruim ou ferramenta ruim
Métodos formais e ferramentas úteis na prática
- Métodos formais e raciocínio automático formam uma área ampla e contam com várias ferramentas
- O conjunto de ferramentas que foi útil no contexto de grandes sistemas de nuvem inclui:
- Linguagens de especificação e model checkers relacionados, como P, TLA+ e Alloy
- Ferramentas de simulação determinística como turmoil
- Usadas com testes e fuzzing para explorar sistematicamente o espaço de estados
- Linguagens de programação voltadas à verificação, como Dafny, e verificadores de código como Kani
- Técnicas de simulação numérica
- Métodos próximos do formalismo, como desenhar tabelas de decisão, tabelas verdade e máquinas de estado explícitas em quadros brancos ou documentos de projeto
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 é um bom ponto de partida para observar métodos formais leves
- Verificar a implementação não é o único objetivo
- Ferramentas como TLA+ e P têm grande valor para revisar projetos de forma mais rápida e concreta antes da implementação
Criar software mais rápido, mais rapidamente
- Quando How Amazon Web Services Uses Formal Methods foi escrito em 2015, o foco era principalmente correção
- Verificar propriedades de segurança e de vivacidade do projeto
- Chegar mais rápido ao projeto correto
- No caso de uma equipe que usava TLA+ em um sistema interno de gerenciamento de locks, o ponto importante era ter “validado otimizações agressivas”
- Ferramentas como TLA+ não apenas ajudam a construir sistemas mais rapidamente, mas também podem ajudar a construir sistemas mais rápidos
- Exploram rapidamente otimizações possíveis
- Encontram as restrições que realmente importam
- Confirmam se a otimização proposta está correta
- Em muitos casos, métodos formais reduzem os difíceis trade-offs entre correção e desempenho em que sistemas costumam cair
O valor de ferramentas usadas na fase de projeto
- Usar, na fase de projeto, ferramentas que ajudam a pensar no desenho do sistema pode aumentar muito a velocidade de desenvolvimento de software
- Isso reduz riscos e permite criar, desde o início, sistemas mais otimizados
- Para engenheiros que constroem sistemas grandes e complexos, métodos formais fazem parte de uma boa prática de engenharia
1 comentários
Comentários do Hacker News
A verificação formal de software, como o próprio texto reconhece, depende muito do tipo de software e do processo de desenvolvimento
Para usar verificação formal, é preciso ter requisitos formais sobre o comportamento do software, mas a maioria dos projetos e filosofias de design não se encaixa nisso. Se desenvolvimento e design avançam juntos quando nem se sabe ao certo o que se quer, fica difícil aplicar métodos formais. Ainda assim, áreas que dependem de especificações antecipadas, como sistemas pequenos e críticos para a segurança, podem se beneficiar muito; software aeroespacial é um exemplo típico
Hoje em dia, não é uma técnica que exija um doutorado ou anos de pesquisa para aprender, e o mesmo vale para escrever especificações básicas de alto nível. Ao usar um verificador de modelos, você aprende algo sobre o sistema que está modelando, e ele é útil mesmo que seja usado apenas para documentação ou treinamento. A força fundamental dos métodos formais está em obrigar você a pensar até o fim. Muitos desenvolvedores acreditam que conseguem implementar algoritmos de concorrência só com a própria cabeça, um verificador de tipos e alguns testes unitários, mas, depois de rodar um verificador de modelos e encontrar erros no design e nas suposições, é inevitável ficar mais humilde. Há muitos sistemas distribuídos menores do que se imagina, e o espaço de estados muitas vezes é bem maior do que se esperava antes de formalizá-lo
Por exemplo, anexei testes baseados em propriedades a uma máquina de estados bastante complicada para garantir que, mesmo que um endpoint fosse chamado com algum input estranho, a máquina de estados interna não fizesse uma transição inválida. O código ao redor não tinha especificação formal, mas a máquina de estados tinha, então isso foi possível; também encontrei bugs sutis que testes unitários tradicionais jamais teriam capturado
Só que, para obter os benefícios dos métodos formais, é preciso comparar o comportamento do programa com algo que não seja o próprio programa, e esse algo também precisa estar escrito em uma linguagem formal. É necessário entender com precisão o comportamento desejado, mas não é preciso cobrir todo o comportamento do software. Testes unitários automatizados também são especificações formais, e executá-los é um método de verificação formal. São apenas especificações e verificações mais fracas do que aquilo que normalmente se chama de métodos formais; não há uma diferença qualitativa clara, nem conceitualmente nem na prática. Se testes são aplicáveis a um software, é bem provável que métodos mais ricos de especificação formal também sejam, e a relação custo-benefício se aprende por tentativa e erro, como se aprende a testar
No fim, é uma questão de quanto dinheiro e tempo a mais se está disposto a gastar para poder chamar isso de “ágil”. Paradoxalmente, a etapa tradicional de requisitos é a mais barata das três abordagens e também a que mais combina com o espírito ágil original, porque converge rapidamente com o cliente no momento em que o custo de mudança é mais baixo: alterar uma linha de texto
Ainda assim, é possível obter o benefício de verificar se nenhum caso foi deixado de fora e se não há contradições dentro do sistema
Sobre métodos formais, vejo com frequência a lógica de que “software é grande, complexo e difícil de acertar; portanto, métodos formais”
Por um lado, eu gostaria que isso fosse verdade. Sou forte no modo acadêmico de aprender, então isso me beneficiaria pessoalmente, e, na prática, também é frustrante ficar procurando a causa quando o software falha porque é de fato complexo. Mas quase nunca se mostra de forma convincente como os métodos formais resolvem esse problema. Este texto é melhor ao apontar que a maior parte do “design” moderno é perda de tempo, mas não explica o suficiente por que TLA é melhor que UML. Soa quase como uma insinuação de que, se você investir meses ou anos em TLA, alcançará uma iluminação e perceberá sua utilidade de um jeito impossível de explicar a quem não a alcançou. Cálculo e estatística bayesiana também têm esse aspecto, então não é algo impossível; mas, no fim, acabo voltando ao julgamento de gerente de projeto: “se fosse realmente tão útil assim, mais gente teria usado e as vantagens teriam ficado evidentes por si só”. Se algo existe há muito tempo e não se consolidou amplamente, provavelmente há um motivo
Quando encontramos um problema difícil de raciocinar, acabamos usando algum “método”. Se for um protocolo de comunicação, é bom explicá-lo como uma máquina de estados, e TLA se encaixa melhor nesse nicho. Ultimamente não tenho visto muitos problemas que justifiquem esse nível de esforço, mas, quando eles aparecem, isso tem um valor enorme. O mesmo vale para linguagens específicas de domínio: para evitar vários problemas, é muito melhor usar um framework de parser do que escrever um parser diretamente. Hoje, a maior parte do retrabalho vem de mudanças de requisitos e de clientes dizendo “não é isso” sem saberem o que realmente querem. Em parte, isso acontece porque as pessoas que fazem as solicitações não pensam o bastante nas implicações do que pedem, mas o fator maior é que o conhecimento necessário para tomar boas decisões não se concentra suficientemente em um só lugar
Métodos formais são claramente um grande investimento. Ainda assim, embora não tenham se estabelecido de modo geral, parte dessas ideias entrou nos sistemas de tipos modernos
A impressão que tive é que o rigor dos verificadores formais impõe limites à complexidade do projeto simplesmente porque a verificação precisa terminar em tempo e memória razoáveis. Talvez a verdadeira vitória de exigir verificação formal seja corrigir o problema de que “software é grande, complexo e difícil de acertar” tornando incômodo lidar com programas grandes e complexos
Eu gostaria de ver descendentes de testes baseados em propriedades que usem técnicas de SAT ou TLA para reduzir rapidamente o espaço de entrada de forma repetível. Por meio de parsing e cobertura de código, deveríamos ser capazes de inferir que passar 12 para uma função não pode tomar um ramo diferente de 11, mas que valores como -1 ou 2^17 < n < 2^32 podem ser diferentes
A maioria dos projetos de software ainda fracassa. Isso não é uma “falha de mercado”; está mais para simplesmente “falhar em construir”
Há, grosso modo, dois ramos nos métodos formais: as técnicas extrínsecas, que ficam separadas do código em si e normalmente inferem especificações do código, e as técnicas intrínsecas, que entram no código e raciocinam sobre ele de forma mais direta
Historicamente, técnicas intrínsecas como sistemas de tipos raciocinavam sobre o código no nível de funções, enquanto técnicas extrínsecas, como verificadores de modelos decidíveis do tipo Spin/P, lidavam com modelos de código descritos por formalismos como autômatos. Vejo o momento atual como uma era de ouro da pesquisa em métodos formais; em comparação com os avanços dos sistemas de tipos e com abordagens intrínsecas impulsionadas por projetos como Verus, parece haver uma tendência de as técnicas extrínsecas serem cada vez menos favorecidas. https://github.com/verus-lang/verus
Já vi a pergunta de como isso funcionaria em uma linguagem com pegada grande, como Rust, mas ainda não vi uma boa resposta. Quero ler mais sobre isso
Pareceu-me que técnicas intrínsecas seriam preferidas porque não exigem escrever e manter uma especificação separada, mas, na prática, não é isso que acontece
Gostei da parte que destaca os métodos formais leves. Manter um conjunto de estratégias de proptest ao lado da base de código não é um investimento muito maior do que escrever testes unitários manuais, mas oferece insights muito melhores graças à cobertura ampla e a casos de falha pequenos e compreensíveis
Acima de tudo, essa abordagem também combina bem com práticas comuns de desenvolvimento de software. https://crates.io/crates/proptest
Sei até certo ponto como escrever bons testes e o esforço envolvido nisso, mas um LLM consegue criar testes melhores muito mais rápido do que eu. Como tarefas repetitivas e entediantes reduzem minha paciência, é bem possível que ele faça menos “de qualquer jeito” do que eu. Se você é engenheiro de software, deveria ter o reflexo de automatizar tarefas que parecem repetitivas; documentação também, hoje em dia, é algo que se gera, o que leva a fazê-la com mais frequência e mais cedo. LLMs podem causar uma pequena revolução na adoção de verificação formal. Gerar especificações corretas é tedioso, mas, se houver contexto suficiente — como código funcional, documentação e dicas —, pode ser uma tarefa relativamente fácil para um LLM. Se eu puder mandar gerar a especificação e depois revisá-la, em vez de escrevê-la inteira diretamente, ficarei muito mais inclinado a fazer isso. Usar Rust também é um sinal de que você valoriza correção, e o compilador dele é provavelmente a ferramenta mais próxima de provar que um sistema está correto sem métodos formais. É provável que seja muito mais fácil do que acrescentar métodos formais a uma linguagem que não tem compilador nem tipos explícitos
A verificação formal de software ainda é difícil demais de usar a ponto de valer a pena, exceto em casos extremos. Em contrapartida, a verificação formal de hardware já chegou a um ponto em que não há motivo para não usá-la
Continuo tentando aprender, mas na maioria dos sistemas é preciso ser um especialista no nível de “alguém que escreveu o próprio compilador”. Por exemplo, tentei provar um codificador/decodificador varint; para 1 ou 2 bytes funcionou, mas além disso não. Quando pedi ajuda, a causa era um detalhe interno impossível de saber, algo como o compilador desenrolar o loop apenas 5 vezes. Ultimamente tenho aprendido Lean e gosto dele, mas acabo encontrando documentação deste tipo: “Definitional equality includes η-equivalence…”. Não estou tentando menosprezar o Lean; pelo contrário, entre as alternativas, sua documentação até parece uma das melhores
Métodos formais não precisam necessariamente ser complexos. O problema é que a maioria deles foi projetada como exercícios acadêmicos para demonstrar algum tópico específico pelo qual um professor se interessava. O TLA+ também é mais próximo de algo projetado para escrever artigos
Entre os métodos formais leves, um de que gosto, embora não seja muito conhecido, é a verificação de traces usando lógica temporal linear: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
Basicamente, basta registrar eventos em logs e, em arquiteturas orientadas a eventos, isso pode vir praticamente de graça. Depois é só rodar predicados como
Always(Locked, Implies(Eventually(Unlocked)))sobre o trace de execução. Dá para aplicar também a traces antigos e combinar com testes de estresse ou fuzzing para explorar o espaço de estados. É simples, poderoso e amplamente aplicável; não precisa de modelo, só dos predicadosMétodos formais implicam uma base abrangente para o comportamento do sistema. Em TLA ou sistemas semelhantes, ainda que seja uma máquina de estados e não o sistema real, a saída é uma prova de que uma propriedade LTL/CTL/TLA vale para todos os comportamentos do sistema, isto é, para todos os traces ou árvores de traces
A discussão anterior aconteceu em junho de 2024: https://news.ycombinator.com/item?id=40753989
15 Years of Formal Methods at AWS: Just Good Engineering Practice? - https://news.ycombinator.com/item?id=40283052 - maio de 2024, 1 comentário
Lento demais. Planejamento logo vira fóssil, e qualquer documento pode ser usado como prova incriminatória no tribunal ágil
A maioria dos textos que li sobre métodos formais parece geração de leads de consultores
Isso em si tudo bem, mas é desagradável quando agem como se tivessem alcançado uma iluminação por meio de métodos formais e prometem corrigir hábitos de programação ruins, até irresponsavelmente perigosos, se eu comprar um pacote de treinamento para meus funcionários ou colegas, ou se eu os contratar. Quando os métodos formais realmente gerarem código de alta qualidade que não possa se desviar da especificação, aí me avisem
Em uma especificação formal, normalmente não se especifica esse nível de detalhe; especifica-se o comportamento geral do sistema. Por isso, uma única especificação muitas vezes corresponde a muitos programas sutilmente diferentes. É também por isso que código é insuficiente como documentação: não dá para saber quais escolhas foram intencionais e quais foram acidentais. Código é concreto demais para explicar requisitos de alto nível. Por outro lado, verificar um programa em relação a uma especificação parece mais viável de implementar
Alguns dos atuais defensores de métodos formais veem quem não os usa como “preguiçoso” ou “burro” e tentam reivindicar superioridade porque eles “fazem a coisa certa” ou “dominaram uma linguagem complexa”
Claro que não são todos, e conheço pessoas boas, mas alguns na verdade se aproximam de pessoas de uma habilidade só. Se você pergunta quais outros sistemas de métodos formais aprenderam ou tentaram nos últimos anos, dizem que estão “ocupados demais” para aprender algo novo. Entre métodos formais recentes e mais fáceis de usar estão o FizzBee, que usa um dialeto de Python e se lê como pseudocódigo; o Quint, com sintaxe mais simples; e o P, com uma sintaxe familiar para usuários de C#. O autor deste texto também já escreveu que métodos formais resolvem apenas metade do seu problema: https://brooker.co.za/blog/2022/06/02/formal.html
Mas o problema mencionado ali já é resolvido pelo PRISM, que nem é novo. Brooker simplesmente não procura ao redor nem tenta aprender