Verificação formal do programa na prática

Tentarei dar uma resposta sucinta a algumas de suas perguntas.Por favor, tenha em mente que este não é estritamente meu campo de pesquisa, então algumas de minhas informações podem estar desatualizadas / incorretas.

1. Existem muitas ferramentas que são especificamente projetadas para provar propriedades formalmente de Java e C ++.

   No entanto, preciso fazer uma pequena digressão aqui: o que significa provar a correção de um programa? O verificador de tipo Java prova uma propriedade formal de um programa Java, ou seja, que certos erros, como adicionar float e int, nunca podem ocorrer! Imagino que você esteja interessado em propriedades muito mais fortes, ou seja, que seu programa nunca entre em um estado indesejado ou que a saída de uma determinada função esteja em conformidade com uma determinada especificação matemática. Em suma, há um amplo gradiente do que pode significar “provar que um programa está correto”, desde propriedades de segurança simples até uma prova completa de que o programa atende a uma especificação detalhada.

   Agora, vou assumir que você está interessado em provar propriedades fortes sobre seus programas. Se estiver interessado em propriedades de segurança (seu programa não pode atingir um determinado estado), em geral, parece que a melhor abordagem é verificação de modelo . No entanto, se você deseja especificar totalmente o comportamento de um programa Java, sua melhor aposta é usar uma linguagem de especificação para essa linguagem, por exemplo JML . Existem linguagens para especificar o comportamento de programas C, por exemplo ACSL , mas eu não sei sobre C ++.

2. Depois de ter suas especificações, você precisa provar que o programa está em conformidade com essas especificações.

   Para isso, você precisa de uma ferramenta que tenha um compreensão formal de ambos sua especificação e a semântica operacional de sua linguagem (Java ou C ++) para expressar o teorema de adequação , ou seja, que a execução do programa respeita a especificação.

   Esta ferramenta também deve permitir que você formule ou gere a prova desse teorema. Agora, essas duas tarefas (especificar e provar) são bastante difíceis, por isso são frequentemente separadas em duas:

   • Uma ferramenta que analisa o código, a especificação e gera o teorema de adequação. Como Frank mencionou, Krakatoa é um exemplo de tal ferramenta.

   • Uma ferramenta que prova o teorema ( s), automática ou interativamente. O Coq interage com o Krakatoa dessa maneira e existem algumas ferramentas automatizadas poderosas, como Z3 , que também podem ser usadas.

   Um (menor) ponto: existem alguns teoremas que são muito difíceis de serem provados com métodos automatizados, e os provadores automáticos de teoremas são conhecidos por ocasionalmente ter bugs de integridade que os tornam menos confiáveis. Esta é uma área onde Coq brilha em comparação (mas não é automático!).

3. Se você deseja gerar código Ocaml, então definitivamente escreva em Coq (Gallina) primeiro, em seguida, extraia o código. No entanto, Coq é péssimo para gerar C ++ ou Java, se é que isso é possível.

4. As ferramentas acima podem lidar com problemas de threading e desempenho? Provavelmente não, as questões de desempenho e threading são melhor tratadas por ferramentas especificamente projetadas, pois são problemas particularmente difíceis. Não tenho certeza se tenho alguma ferramenta para recomendar aqui, embora o projeto de Martin Hofmann “s PolyNI pareça interessante.

Em conclusão: a verificação formal de programas Java e C ++ do “mundo real” é um campo grande e bem desenvolvido, e o Coq é adequado para partes dessa tarefa. Você pode encontrar uma visão geral de alto nível aqui , por exemplo.

Comentários

• Obrigado por esta postagem e as referências que você adicionou. IMHO, o objetivo dos engenheiros de software é ser capaz de lançar rapidamente sistemas que 1) sempre forneçam resultados corretos, 2) nunca falhem. Eu posso ver um problema de regressão aqui, onde você pode querer provar que a especificação em si é ” livre de erros ” 🙂 meio que como tentar definir ” proposição verdadeira de uma linguagem ” com uma meta-linguagem, então precisando de outra meta-linguagem para isso, depois outra um …
• O problema é que o que o usuário ” deseja ” geralmente não é expresso de forma formal língua! Geralmente não há uma resposta formal para a pergunta: ” esta especificação formal está de acordo com minha ideia informal? “. É ‘ possível testar uma especificação formal e provar que ela tem certas propriedades matemáticas, mas no final você precisa relacionar a matemática ao mundo real, que é um processo não formal.
• Sim, claro – eu sempre percebi que os métodos formais só podiam começar de um ponto bem definido.Se essa especificação está em conformidade ou não com as necessidades conscientes / inconscientes / não descobertas dos usuários da vida real é outro problema, não endereçável com métodos formais (mas certamente um problema para engenheiros).
• Um teorema é por definição um proposição comprovada. Portanto, você provavelmente não pretende ” provar o teorema “.
• @nbro A Wikipedia parece concordar contigo. Mathworld, no entanto, define um teorema como uma proposição que ” pode ser demonstrada como verdadeira por operações matemáticas aceitas “. Neste caso, dar provas de teoremas não só é possível, mas necessário para justificar chamá-los assim! 🙂 (este é um contra-problema, claro)

Eu gostaria de mencionar três aplicações notáveis de métodos formais / ferramentas de verificação formal na indústria ou sistemas reais não triviais. Observe que tenho pouca experiência neste tópico e só os aprendo lendo artigos.

1. A ferramenta de código aberto Java Pathfinder (JPF para abreviar) lançado pela NASA em 2005 é um sistema para verificar programas de bytecode Java executáveis (consulte Java Pathfinder @ wiki ). Ele tem sido usado para detectar inconsistências no software executivo do K9 Rover da NASA Ames.

2. Este artigo: Usando a verificação de modelo para encontrar erros graves do sistema de arquivos @ OSDI “04 mostra como usar verificação de modelo para encontrar erros graves em sistemas de arquivos. Um sistema chamado FiSC é aplicado a três sistemas de arquivos amplamente usados e amplamente testados: ext3, JFS e ReiserFS, e 32 bugs sérios são encontrados. Ele ganhou o prêmio de melhor artigo.

3. Este artigo: Como Amazon Web Services usa métodos formais @ CACM “15 descreve como a AWS aplica métodos formais para seus produtos como S3, DynamoDB, EBS e gerenciador de bloqueio distribuído interno. Ele se concentra na ferramenta TLA + de Lamport. A propósito, Lamport tem usado intensivamente sua própria caixa de ferramentas de TLA. Ele geralmente fornece uma verificação formal (bastante completa) em TLA dos algoritmos / teoremas propostos por ele mesmo (bem como pelos co-autores) nos apêndices dos artigos.

Um formal A especificação de um programa é (mais ou menos) um programa escrito em outra linguagem de programação. Como resultado, a especificação certamente incluirá seus próprios bugs.

A vantagem da verificação formal é que, como o programa e a especificação são duas implementações separadas, seus bugs serão diferentes. Mas nem sempre: uma fonte comum de bugs, casos negligenciados, geralmente correspondem. Assim, a verificação formal não é uma panacéia: ela ainda pode deixar passar um número não trivial de bugs.

Uma desvantagem da verificação formal é que ela pode impor algo como o dobro do custo de implementação, provavelmente mais (você precisa um especialista em especificação formal, e você precisa usar as ferramentas mais ou menos experimentais que vêm com ele; isso não sairá barato).

Eu acho que configurar casos de teste e andaimes para executá-los automaticamente seria um melhor uso do seu tempo.

Comentários

• A vantagem da verificação formal é que … . Uma segunda desvantagem da verificação formal é que … Isso é confuso.
• Acho que a incompatibilidade entre a especificação e a tarefa informal é um problema de análise de requisitos de software, não de programação.

Você faz algumas perguntas diferentes. Concordo que parece que os métodos de verificação formal para aplicações industriais / comerciais não são tão comuns. deve-se perceber, entretanto, que muitos princípios de “verificação formal” são incorporados aos compiladores para determinar a correção do programa! então, de certa forma, se você usa um compilador moderno, está usando muito do que há de mais moderno em verificação formal.

Você diz “Estou cansado de testar”, mas verificação formal não é realmente um substituto para o teste. de certa forma, é uma variação dos testes.

Você mencionou o Java.existem muitos métodos de verificação formais avançados incorporados a um programa de verificação java chamado FindBugs que de fato pode ser executado em grandes bases de código. Observe que haverá “falsos positivos e falsos negativos” e os resultados precisam ser revisados / analisados por um desenvolvedor humano. Mas observe que, mesmo que ele não esteja revelando defeitos funcionais reais, ele geralmente exibe “antipadrões” que devem ser evitados no código de qualquer maneira.

Você não faz mais menção a seu aplicativo específico, exceto “industrial” . A verificação formal na prática tende a depender da aplicação particular.

As técnicas de verificação formal parecem ser amplamente utilizadas em EE para provar a correção do circuito, por exemplo, no projeto de microprocessador.

Aqui está um exemplo de uma pesquisa de ferramentas de verificação formal no campo EE por Lars Philipson .

Comentários

• ‘ é enganoso dizer que ” a muitos ” princípios de verificação formal ” são incorporados aos compiladores para determinar a exatidão do programa “. O que você se refere é a verificação de tipo estática que alguns compiladores fazem, mas as propriedades verificadas dessa forma são bastante simples, por exemplo, evitando adicionar um número e uma string. Isso é útil, mas muito longe do que normalmente é entendido por ” verificação formal “.
• não consulte especificamente a verificação de tipo estático, embora esse seja um exemplo simples / comum. As técnicas de otimização do compilador imho, que são amplamente difundidas e avançadas, são aproximadamente semelhantes aos princípios de verificação formal, porque envolvem técnicas avançadas para determinar / mostrar a equivalência de variantes de programa otimizadas. então parece que é importante evitar o problema ” mover postes ” aqui e não presumir que simplesmente porque um compilador o faz ou é construído no compilador, não é uma verificação formal.
• concordou que isso não é um entendimento comum. as técnicas de otimização estão, grosso modo, criando um modelo de comportamento de programa, por exemplo, de um loop ou sub-rotina, e otimizando esse modelo e, em seguida, gerando um novo código que é comprovadamente equivalente. portanto, algumas dessas otimizações são bastante sofisticadas na reorganização do código & para mim, elas fazem uso de princípios de verificação formal. parece haver muitos outros exemplos de métodos de verificação formal no compilador … a pergunta original fez muitas perguntas diferentes, como muitos notaram, defn não estou tentando responder a todas as perguntas nela contidas.
• pelo forma parece haver alguns princípios de verificação formal também usados no JRE, mecanismo de tempo de execução java, por exemplo, otimização dinâmica, etc …
• isto é ” o sonho da verificação formal ” referido pelo filmus acima, imho uma abstração quimérica, e a indústria pragmática / utilitária / realista em grande parte o reconhece como tal. grandes bases de código são conhecidas há décadas por terem $ x $ bugs / defeitos por $ y $ K-linhas de código e isso nunca mudará, não importa o quanto a teoria / tecnologia avance, é um fato de natureza humana . e, de fato, teoremas matemáticos criados por humanos têm as mesmas propriedades, embora isso não seja muito apreciado!

Talvez um verificador de modelo possa ser útil.

http://alloytools.org/documentation.html Alloy é um verificador de modelo .

Uma boa apresentação explicando o conceito de verificação de modelo usando Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

Na mesma família de ferramentas vem o “teste baseado em propriedade”, todos eles tentam encontrar um contra-exemplo para o modelo de especificação dado de seu software.