Métodos formais: apenas uma boa prática de engenharia? (2024)

• Introdução

  • Marc Brooker é um engenheiro da AWS que trabalha com bancos de dados e sistemas serverless, e enfatiza a importância dos métodos formais na engenharia de software.

• Importância dos métodos formais

  • Métodos formais são essenciais para economizar tempo e custos em sistemas de grande escala, sistemas distribuídos e sistemas críticos de baixo nível.
  • Engenharia de software é um exercício de otimização de tempo e custo.
  • Métodos formais reduzem o custo de retrabalho e tratam mudanças de interface cedo, aumentando a velocidade e a eficiência do desenvolvimento de software.

• Escopo de aplicação dos métodos formais

  • Em softwares guiados por requisitos de usuário que mudam rapidamente, o valor dos métodos formais pode ser limitado.
  • Em sistemas de grande escala, distribuídos e de baixo nível, métodos formais reduzem significativamente o retrabalho e a densidade de bugs.

• Métodos formais e ferramentas

  • Métodos formais e raciocínio automatizado incluem várias ferramentas e são usados de forma útil nos sistemas de nuvem de grande escala da AWS.
  • Há linguagens de especificação como TLA+, P e Alloy, além de model checkers, ferramentas de simulação determinística e linguagens de programação com suporte à verificação.

• Conclusão

  • Ferramentas que ajudam a pensar no design do sistema na fase de projeto aceleram o desenvolvimento de software, reduzem riscos e permitem desenvolver sistemas melhores.
  • Para engenheiros que lidam com sistemas grandes e complexos, métodos formais fazem parte de boas práticas de engenharia.

[GN⁺]

Opiniões do Hacker News

• A verificação formal de software depende bastante do tipo de software e do processo de desenvolvimento. A maioria dos projetos de software não é compatível com requisitos formais

  • O desenvolvimento e o design de software muitas vezes acontecem em paralelo, mas isso não se encaixa bem em métodos formais
  • Sistemas críticos de segurança, como software aeroespacial, podem se beneficiar bastante da verificação formal

• A alegação de que métodos formais podem resolver a complexidade do software aparece com frequência

  • Isso pode ser atraente para quem prefere abordagens acadêmicas
  • No entanto, faltam casos convincentes de como métodos formais de fato resolvem problemas na prática
  • Há uma sugestão implícita de que, ao aprender ferramentas como TLA, é possível entender sua utilidade

• Há dois tipos principais de métodos formais: técnicas extrínsecas, separadas do código, e técnicas intrínsecas, que acompanham o código

  • As técnicas intrínsecas operam no nível funcional do código, enquanto as extrínsecas analisam formalmente modelos do código
  • Estamos atualmente em uma era de ouro da pesquisa em métodos formais, e as técnicas intrínsecas vêm recebendo mais atenção

• Métodos formais leves podem ser mantidos junto com a base de código e oferecem mais insights do que testes unitários

  • Essa abordagem combina bem com práticas comuns de desenvolvimento de software

• A verificação formal de software continua sendo uma tarefa muito difícil e só vale a pena em casos extremos

  • Exige conhecimento de nível especializado e, para a maioria dos sistemas, é extremamente complexa
  • Aprender ferramentas como Lean é difícil, mas a documentação é boa

• Muitos artigos sobre métodos formais parecem geração de leads para consultores

  • É melhor esperar até que métodos formais realmente passem a produzir código de alta qualidade

• Um dos métodos formais leves é a verificação de rastros usando Linear Temporal Logic

  • É uma forma simples e poderosa de registrar eventos e executar condições sobre rastros de execução

• Métodos formais modernos como TLA+ e Alloy são tão fáceis de aprender quanto Python

  • Muitos sistemas de nuvem já foram verificados com essas ferramentas (por exemplo: Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB)