Como podemos saber que métodos formais funcionam?

Um objetivo importante dos métodos formais é provar a correção dos sistemas, por meios automatizados ou direcionados ao homem. No entanto, parece que, mesmo que você possa fornecer uma prova de correção, NÃO poderá garantir que o sistema não falhará. Por exemplo:

• A especificação pode não modelar o sistema corretamente, ou um sistema de produção pode ser muito complicado para modelar ou o sistema pode ter falhas inerentes devido a requisitos contraditórios. Que técnicas são conhecidas para testar se uma especificação faz algum sentido?
• O processo de prova também pode falhar! Quem sabe que essas regras de inferência são corretas e legítimas? Além disso, as provas podem ser muito grandes, e como sabemos que elas não contêm erros? Este é o coração da crítica nos "Processos sociais e provas de teoremas e programas" de De Millo, Lipton e Perlis. Como os pesquisadores de métodos formais modernos respondem a essa crítica?
• No tempo de execução, existem muitos eventos e fatores não determinísticos que podem afetar seriamente o sistema. Por exemplo, os raios cósmicos podem alterar a RAM de maneiras imprevisíveis e, geralmente, não temos garantias de que o hardware não sofra falhas bizantinas, o que Lamport provou ser muito difícil de ser robusto. Portanto, a correção do sistema estático não garante que o sistema não falhe! Existem técnicas conhecidas para explicar a falibilidade de hardware real?
• Atualmente, o teste é a ferramenta mais importante que temos para estabelecer que o software funciona. Parece que deveria ser uma ferramenta complementar com métodos formais. No entanto, vejo principalmente pesquisas focadas em métodos ou testes formais. O que se sabe sobre a combinação dos dois?

Em relação a 4: há muito trabalho combinando métodos e testes formais. O "teste formal de métodos" no Google revela uma grande quantidade de trabalho. Embora existam muitos objetivos diferentes para esse trabalho, um dos principais objetivos é gerar conjuntos de testes mais eficazes. Esta palestra fornece uma boa introdução, baseada na verificação de modelos.

Também com relação à questão da segurança do software , que foi editada fora de questão: os métodos formais precisam trabalhar mais para entregar nesse domínio. Normalmente, escreve-se uma especificação para um software e verifica se a especificação é atendida, ou seja, quando a entrada satisfaz a pré-condição de que a saída satisfaz a pós-condição. Para garantir um software seguro, também é necessário verificar também se o software se comporta de maneira sensata para entradas que não atendam às condições prévias. (É claro que isso equivale a definir a condição prévia como verdadeira para todas as entradas.) O espaço de todas as entradas é tipicamente muito maior do que apenas entradas bem formadas, mas geralmente é um local em que mesmo software funcionalmente correto pode ser violado, simplesmente por violando suas suposições.

Em relação ao ponto 3: Alguns trabalhos foram feitos para verificar os sistemas em configurações nas quais as falhas são explicitamente modeladas, incluindo Lógica defeituosa: raciocínio sobre programas tolerantes a falhas. Matthew Meola e David Walker. Simpósio Europeu de Programação, 2010. O trabalho de verificação probabilística de modelos e verificação probabilística certamente também aborda a questão das falhas em algum grau.

Seus pontos em ordem:

• A exatidão de todas as especificações é finalmente subjetiva: elas são percebidas para resolver um problema corretamente de acordo com seus usuários ou não. Não há como fugir disso, é o desenvolvimento de software, e nenhum método tem a bala de prata para este.
• Muito trabalho é feito para provar que o processo está correto com relação a suas suposições. Geralmente, há informações disponíveis para os especialistas validarem essas regras. Qualquer atividade humana está sujeita a erros, mas sistemas muito formalizados, usando abordagens bem estudadas, são muito menos sujeitos a erros do que quase todos os outros processos humanos.
• Em algum momento, qualquer sistema possui um modo de falha fora do escopo desse sistema. Ainda é melhor eliminar todas as fontes previsíveis de erro, mesmo se você deixar algumas imprevisíveis sem explicação.
• Testes e provas podem coexistir facilmente. O teste é um processo menos específico e mais ad hoc ; portanto, você poderá encontrar um trabalho menos formal. Mas você pode estar interessado em uma ferramenta como o QuickCheck que complementa com testes as provas oferecidas pelo sistema do tipo Haskell.

Métodos formais já demonstraram funcionar em grande escala. Sem eles, não teríamos conseguido lidar com a complexidade de projetar sistemas digitais modernos (microprocessadores).

Nenhum micro navio sem sua lógica sujeita a verificação de equivalência funcional; sem que sua FPU tenha sido sujeita a FV; sem que seus protocolos de coerência de cache tenham sido sujeitos a VF (esse é o caso desde 1995).

Exceto diferenças óbvias entre software e sistemas físicos projetados (por exemplo, pontes, onde é possível adicionar fatores de segurança), eles desempenham o papel da matemática de engenharia no CS. No entanto, o uso da FM sempre depende do benefício / custo. O teste de fuzz compensa muito em empresas como a Microsoft (Google SAGE em um slide).

Mesmo dentro de um micro, existem subsistemas (por exemplo, pipelines de microprocessadores), nos quais o FV não teve o mesmo impacto que em outros lugares (por exemplo, FPU, onde o teste convencional não foi realizado em muitos casos em que a avaliação formal da trajetória simbólica provou a ausência de bugs) : Kaivola e cols. CAV'09).

Métodos formais também estão sendo usados ​​na síntese de artefatos (código, testes de alta qualidade, agendas para a drenagem ideal de bancos de baterias, ...). Obviamente, todas as questões levantadas na pergunta são bastante válidas e, como em qualquer outro uso da tecnologia, anúncios falsos devem ser reconhecidos e evitados.

Em relação a 2: se o sistema é formalizado em um assistente de prova (por exemplo, Twelf ou Agda ou Coq) e as propriedades de solidez e integridade são verificadas, e as provas são feitas nessa codificação, isso não é problema. Você pode ter formalizado um sistema que não está descrevendo o que pretendia, mas pelo menos não terá provas incorretas ou um sistema quebrado no qual está raciocinando.

No entanto, parece que, mesmo que você possa fornecer uma prova de correção, NÃO poderá garantir que o sistema não falhará.

Sim, talvez não haja garantias . Métodos formais têm como objetivo encontrar e eliminar erros e convencer os humanos.

Que técnicas são conhecidas para testar se uma especificação faz algum sentido?

Você pode estar interessado em ferramentas de verificação de modelo para especificações de sistemas formais .

O processo de prova também pode falhar! Quem sabe que essas regras de inferência são corretas e legítimas?

Eu acho que (por causa do teorema da incompletude de Goedel) mostrar que um sistema de regras de inferência é consistente apela necessariamente a um conjunto ainda mais poderoso de regras de inferência.

Além disso, as provas podem ser muito grandes, e como sabemos que elas não contêm erros?

Felizmente, grandes provas são verificadas por um pequeno verificador de provas que pode ser lido e compreendido por humanos em um período de tempo razoável. Isso às vezes é chamado de "critério de Bruijn". Se você acredita que o verificador de provas não certifica uma prova incorreta, basta verificar o verificador.

Existem técnicas conhecidas para explicar a falibilidade de hardware real?

E a linguagem assembly digitada tolerante a falhas ?

No entanto, vejo principalmente pesquisas focadas em métodos ou testes formais. O que se sabe sobre a combinação dos dois?

"A conferência TAP é dedicada à convergência de provas e testes" .

Apenas pesquisar no Google "provas e testes" tem vários bons resultados acima da dobra.

Que técnicas são conhecidas para testar se uma especificação faz algum sentido?

É definitivamente uma decisão judicial. Na engenharia de software, as pessoas criaram uma metodologia muito rigorosa para encontrar / escrever / confirmar as especificações. Isso é feito por humanos reais e usando um processo não formal (no sentido não matemático), por isso ainda está sujeito a inconsistência, mas no final do dia, corresponde ao que as pessoas querem verificar, nem mais nem menos.

Existem técnicas conhecidas para explicar a falibilidade de hardware real?

Claro, existe um campo de verificação conhecido como verificação de tempo de execução ; você também pode usar a verificação de modelo baseada em execução no sistema real em execução em um ambiente totalmente virtual, sujeito a um cenário específico (eu contribuí com o V-DS + APMC ). No entanto, esse é claramente um grande problema para adicionar a interação entre o sistema e o ambiente no processo de verificação.

No entanto, vejo principalmente pesquisas focadas em métodos ou testes formais. O que se sabe sobre a combinação dos dois?

Uau, hoje vou ser totalmente sem vergonha e me citar de novo. Com os co-autores, trabalhamos na combinação de verificação e teste de modelo, você pode consultar a lista de publicações de um ex-aluno de doutorado de nosso grupo ou procurar "verificação probabilística aproximada de modelo" ou "verificação estatística de modelo" em qualquer bom mecanismo de pesquisa (trabalho realizado por Younes et al., Sen et al. Ou eu et al. E muitos outros).

Você pode estar muito interessado nas obras de John Rushby , um dos projetistas do provador do teorema do PVS, que é genericamente interessado exatamente nos pontos mencionados. Você pode ler este relatório clássico para a FAA sobre o uso de Métodos Formais e a Certificação de Sistemas Críticos (1993) , e seus escritos mais recentes sobre a montagem de um caso de segurança formal e probabilístico a partir de vários meios de evidência fornecidos (testes, provas, análises, etc).