Verificação formal do programa na prática

66

Como engenheiro de software, escrevo muitos códigos para produtos industriais. Coisas relativamente complicadas com classes, threads, alguns esforços de design, mas também alguns compromissos de desempenho. Eu faço muitos testes e estou cansado de testar, então fiquei interessado em ferramentas formais de prova, como Coq, Isabelle ... Posso usar uma delas para provar formalmente que meu código está livre de erros e está pronto com isso? - mas cada vez que verifico uma dessas ferramentas, deixo de me convencer de que elas são utilizáveis ​​na engenharia de software cotidiana. Agora, isso poderia ser apenas eu, e estou procurando dicas / opiniões / idéias sobre isso :-)

Especificamente, tenho a impressão de que fazer com que uma dessas ferramentas funcione para mim exigiria um grande investimento para definir adequadamente para o provador os objetos, métodos ... do programa em consideração. Então eu me pergunto se o provador não ficaria sem força, dado o tamanho de tudo o que teria que lidar. Ou talvez eu tivesse que me livrar dos efeitos colaterais (essas ferramentas de teste parecem se sair muito bem com linguagens declarativas) e me pergunto se isso resultaria em "código comprovado" que não poderia ser usado porque não seria rápido ou pequeno o suficiente. Além disso, não tenho o luxo de alterar a linguagem com a qual trabalho, ela precisa ser Java ou C ++: não posso dizer ao meu chefe que vou codificar no OXXXml a partir de agora, porque é a única linguagem em que posso provar a correção do código ...

Alguém com mais experiência em ferramentas formais de prova pode comentar? Mais uma vez - eu AMO usar uma ferramenta formal, provador, eu acho que eles são grandes, mas tenho a impressão de que eles estão em uma torre de marfim que eu não posso chegar da vala humilde de Java / C ++ ... (PS: I Também AMO Haskell, OCaml ... não entendi errado: sou fã de linguagens declarativas e provas formais, só estou tentando ver como eu poderia realisticamente tornar isso útil para a engenharia de software)

Atualização: Como isso é bastante amplo, vamos tentar as seguintes perguntas mais específicas: 1) existem exemplos de uso de provadores para provar a exatidão de programas industriais Java / C ++? 2) Coq seria adequado para essa tarefa? 3) Se Coq for adequado, devo escrever o programa em Coq primeiro e gerar C ++ / Java a partir de Coq? 4) Essa abordagem poderia lidar com otimizações de encadeamento e desempenho?

programming-languages program-correctness software-verification Frank
fonte
3
Entendo e aprecio o seu problema, mas não entendo o que é essa pergunta (como um post no SE). Discussão? Experiência? Nem é adequado para SE. O "O que eu posso fazer?" o tom me faz sentir que essa é uma pergunta muito ampla também.
Raphael
3
Entendo ... Concordo que esta questão não foi formulada claramente. Então, digamos: 1) existem exemplos de uso de provadores para provar a correção de programas industriais Java / C ++? 2) Coq seria adequado para essa tarefa? 3) Se o Coq for adequado, devo escrever o programa no Coq primeiro, para que o Coq gere C ++ / Java a partir disso? 4) Essa abordagem poderia lidar com otimizações de encadeamento e desempenho?
19413 Frank
2
Então são quatro perguntas, então. 1) provavelmente é melhor para a Engenharia de Software, uma vez que é improvável que você encontre (muitos) profissionais do setor aqui. 2) tem um gosto um tanto subjetivo, mas podemos ter pessoas aqui que podem oferecer uma perspectiva objetiva. 3) é, tanto quanto posso dizer, completamente subjetivo. 4) É uma boa pergunta para este site. Em resumo: separe suas perguntas, vá para a Engenharia de Software com a primeira e pense bem se pode esperar uma resposta objetiva (!) Aqui (!) Antes de postar 2).
Raphael
10
Você está descrevendo o sonho da verificação formal, mas estamos muito longe de estar lá. AFAIK, verificação de programa é uma tarefa não rotineira e se aplica apenas a programas muito simples. Dito isso, acho que essa pergunta é direta para o site e eu agradeceria a alguém da área que admitisse os limites de seu campo, explicando o estado da arte e as limitações (talvez vinculando a alguma pesquisa) )
Yuval Filmus
9
O problema com a verificação de programas em C ++ é que o C ++ não é uma linguagem bem definida. Não acho que a verificação em larga escala seja possível até que muitas partes dos sistemas de software (SO, bibliotecas, linguagens de programação) sejam redesenhadas para dar suporte à verificação. Como é sabido, você não pode simplesmente despejar 200000 linhas de código em alguém e dizer "verificar!". Você precisa verificar e escrever o código juntos e adaptar seus hábitos de programação ao fato de também estar verificando.
Andrej Bauer

Respostas:

35

Tentarei dar uma resposta sucinta a algumas de suas perguntas. Lembre-se de que este não é estritamente meu campo de pesquisa; portanto, algumas das minhas informações podem estar desatualizadas / incorretas.

  1. Existem muitas ferramentas projetadas especificamente para provar formalmente propriedades 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 um floate um int, nunca podem ocorrer! Eu imagino que você esteja interessado em propriedades muito mais fortes, a saber: seu programa nunca pode entrar 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 resumo, existe um amplo gradiente do que "provar um programa correto" pode significar, desde simples propriedades de segurança 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 você estiver interessado em propriedades de segurança (seu programa não pode atingir um determinado estado), em geral, parece que a melhor abordagem é a verificação de modelo . No entanto, se você deseja especificar completamente 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 em C, por exemplo ACSL , mas não sei sobre C ++.

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

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

    Essa 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, portanto são frequentemente separadas em duas:

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

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

    Um ponto (menor): existem alguns teoremas muito difíceis de serem provados com métodos automatizados, e sabe-se que os provadores automáticos de teoremas ocasionalmente têm bugs de sonoridade que os tornam menos confiáveis. Esta é uma área em que a Coq brilha em comparação (mas não é automática!).

  3. Se você deseja gerar o código Ocaml, escreva definitivamente em Coq (Gallina) primeiro e depois extraia o código. No entanto, Coq é péssimo na geração de C ++ ou Java, se for possível.

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

Concluindo: a verificação formal dos programas Java e C ++ do "mundo real" é um campo amplo 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.

cody
fonte
Obrigado por este post e pelas referências que você adicionou. IMHO, o objetivo dos engenheiros de software é poder liberar rapidamente sistemas que 1) sempre forneçam resultados corretos, 2) nunca falhem. Eu pude ver um problema de regressão aqui, onde você pode provar que a especificação em si é "livre de bugs" :-) meio como tentar definir "proposição verdadeira de uma linguagem" com uma meta-linguagem, precisando de outra meta- idioma para que, depois outro ...
Frank
6
O problema é que o que o usuário "deseja" geralmente não é expresso em uma linguagem formal! Geralmente, não há resposta formal para a pergunta: "essa especificação formal está de acordo com minha ideia informal?". É possível testar uma especificação formal e provar que ela possui certas propriedades matemáticas, mas, no final das contas, você precisa relacionar a matemática ao mundo real, que é um processo não formal.
Cody
Sim, é claro - sempre percebi que os métodos formais só podiam começar de um ponto bem definido. Se essa especificação está de acordo ou não com as necessidades conscientes / inconscientes / não descobertas dos usuários da vida real, é outro problema, não solucionável com métodos formais (mas certamente um problema para os engenheiros).
Frank
Um teorema é, por definição, uma proposição comprovada. Então, você provavelmente não pretende "provar o teorema".
nbro
A Wikipedia @ nbro parece concordar com você. Mathworld, no entanto, define um teorema como uma proposição que " pode ser demonstrada verdadeira por operações matemáticas aceitas". Nesse caso, fornecer provas de teoremas não é apenas possível, mas necessário para justificar chamá-los assim! :) (este é um counterquibble, é claro)
cody
15

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

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

  2. Este documento: Usando a Verificação de Modelo para Encontrar Erros Graves no Sistema de Arquivos @ OSDI'04 mostra como usar a verificação de modelo para encontrar erros graves nos sistemas de arquivos. Um sistema chamado FiSC é aplicado a três sistemas de arquivos amplamente utilizados e altamente testados: ext3, JFS e ReiserFS e 32 bugs graves. Ele ganhou o prêmio de melhor artigo.

  3. Este documento: Como o Amazon Web Services usa métodos formais @ CACM'15 descreve como a AWS aplica métodos formais a seus produtos, como S3, DynamoDB, EBS e Internal Distributed Lock Manager. Ele se concentra na ferramenta TLA + da Lamport . A propósito, Lamport usou intensivamente sua própria caixa de ferramentas TLA. Ele geralmente dá uma verificação formal (bastante completa) no TLA dos algoritmos / teoremas propostos por ele (e também pelos co-autores) em apêndices aos artigos.

hengxin
fonte
4

Uma especificação formal 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 erros.

A vantagem da verificação formal é que, como o programa e a especificação são duas implementações separadas, seus erros serão diferentes. Mas nem sempre: uma fonte comum de bugs, casos negligenciados, geralmente corresponde. Assim, a verificação formal não é uma panacéia: ainda pode perder 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 de um especialista em especificação formal e precisa usar as ferramentas mais ou menos experimentais que a acompanham; isso não sai barato )

Eu acho que configurar casos de teste e andaimes para executá-los automaticamente seria uma melhor utilização do seu tempo.

vonbrand
fonte
A vantagem da verificação formal é que ... Uma segunda desvantagem da verificação formal é que ... Isso é confuso.
Hengxin
Eu acho que a incompatibilidade entre especificação e tarefa informal é um problema de análise de requisitos de software, não um problema de programação.
Kaveh
3

A verificação formal agora é possível para programas gravados em um subconjunto de C ++ projetado para sistemas embarcados críticos para a segurança. Veja http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt para uma breve apresentação e http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf para o artigo completo.

dc42
fonte
5
Obrigado pelos links. Pelo menos uma breve visão geral de seu conteúdo seria útil para se proteger contra a podridão de links, especialmente porque seus links são para um site corporativo: eles tendem a se reorganizar periodicamente, matando todos os links no site.
precisa saber é o seguinte
2

Você faz algumas perguntas diferentes. Concordo que parece que os métodos formais de verificação para aplicações industriais / comerciais não são tão comuns. No entanto, deve-se perceber que muitos princípios de "verificação formal" são incorporados aos compiladores para determinar a correção do programa! de certa forma, se você usa um compilador moderno, está usando grande parte do estado da arte na verificação formal.

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

Você menciona Java. existem muitos métodos formais avançados de verificação incorporados a um programa de verificação java chamado FindBugs, que de fato podem ser executados em grandes bases de código. Observe que ele exibirá "falsos positivos e falsos negativos" e os resultados precisam ser revisados ​​/ analisados ​​por um desenvolvedor humano. Mas observe que, mesmo que não esteja aparecendo defeitos funcionais reais, geralmente aparecem "antipatterns" que devem ser evitados no código de qualquer maneira.

Você não menciona mais sua aplicação específica, exceto "industrial". A verificação formal na prática tende a depender da aplicação específica.

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

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

vzn
fonte
2
É enganoso dizer que "muitos princípios de" verificação formal "estão embutidos nos compiladores para determinar a correção do programa". A que você se refere é a verificação de tipo estática, que alguns compiladores fazem, mas as propriedades verificadas dessa maneira são bastante simples, por exemplo, evitando adicionar um número e uma string. Isso é útil, mas está muito longe do que geralmente é entendido pela "verificação formal".
Martin Berger
2
não se referiu especificamente à verificação de tipo estático, embora esse seja um exemplo simples / comum. As técnicas de otimização de compilador imho, generalizadas e avançadas, são praticamente semelhantes aos princípios formais de verificação, porque envolvem técnicas avançadas para determinar / mostrar equivalência de variantes de programa otimizadas. portanto, parece importante evitar o problema "mover metas" aqui e não assumir que, simplesmente porque um compilador faz isso ou é incorporado ao compilador, não é uma verificação formal.
vzn
2
concordou que este não é um entendimento comum. as técnicas de otimização basicamente estão criando um modelo de comportamento do 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 e, para mim, usam os princípios formais de verificação. parece haver muitos outros exemplos de métodos formais de verificação no compilador ... a pergunta original fez muitas perguntas diferentes, como muitos observaram, não estou tentando responder a todas as perguntas nele contidas.
vzn
2
por sinal, parece haver alguns princípios de verificação formal também utilizados no JRE, java motor de tempo de execução, por exemplo, otimização dinâmica, etc ...
vzn
3
esse é "o sonho da verificação formal", referido pelo filmus acima, em uma abstração quimérica, e a indústria pragmática / utilitária / realista o reconhece amplamente como tal. Sabe-se há décadas que grandes bases de código possuem erros / defeitos por linhas K de código e isso nunca muda, independentemente do avanço da teoria / tecnologia, é um fato da natureza humana . e, de fato, os teoremas matemáticos criados pelo homem têm as mesmas propriedades, embora isso não seja amplamente apreciado! yxy
vzn
1

Talvez um verificador de modelos possa ser útil.

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

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

Na mesma família de ferramentas, vem os 'testes baseados em propriedades', todos tentam encontrar um contra-exemplo para o modelo de especificação fornecido pelo seu software.

ticktock
fonte