Estou tentando me ensinar diferentes abordagens à verificação de software. Eu li alguns artigos. Até onde eu aprendi, a lógica proposicional com temporal geralmente usa verificação de modelo com solucionadores SAT (em sistemas reativos contínuos), mas e a lógica de primeira ordem com temporal? Ele usa provadores de teoremas? Ou também pode usar o SAT?
Qualquer sugestão de livros ou artigos para iniciantes neste assunto é muito apreciada.
Respostas:
A lógica de primeira ordem é indecidível, portanto, a solução SAT não ajuda muito. Dito isto, existem técnicas para verificação de modelo limitado de fórmulas de primeira ordem. Isso significa que apenas um número fixo de objetos pode ser considerado ao tentar determinar se a fórmula é verdadeira ou falsa. Claramente, isso não está completo, mas se um contra-exemplo for encontrado, ele realmente será um contra-exemplo.
A ferramenta Alloy é uma ferramenta que permite que os modelos sejam descritos na lógica de primeira ordem (embora a sintaxe da superfície seja baseada em modelos descritos relacionalmente) e usa a verificação limitada de modelos para encontrar soluções. Um solucionador SAT é usado sob o capô. Uma extensão de liga permite modelos com caráter temporal, embora tecnicamente não suporte a lógica temporal.
Se você deseja explorar mais, por exemplo, para verificar a correção do programa, consulte as ferramentas de verificação do programa. Geralmente, elas são baseadas na lógica Hoare (para raciocinar sobre pré e pós-condições), possivelmente estendidas com a lógica de Separação (para raciocinar sobre pilhas). Essas lógicas são geralmente indecidíveis, portanto, é necessária uma certa quantidade de interação entre o ser humano e a ferramenta de verificação. Alguns exemplos de ferramentas são:
fonte
Depois de ler sua pergunta, a única maneira que eu pude ver e ter conhecimento suficiente para unir os tópicos foi fornecer um conjunto de artigos de alto nível que detalha a verificação de software e tenta unir a verificação de modelos e a prova de teoremas. Espero que meu comentário tenha feito isso:
Dê uma olhada na verificação de software , em seguida, a verificação formal , em seguida, verificação de modelo e de verificação Software Formal: Modelo Verificação e teoremas
Dave deu uma boa resposta, pela qual não posso fazer muito mais justiça à primeira parte da pergunta do que Dave, pois também sou novo nisso.
Como esta é sua primeira pergunta em um site da SE , a razão pela qual eu não dei uma resposta, mas um comentário é porque aqui uma resposta não pode ser apenas um conjunto de links, mas deve dar uma resposta por escrito e usar links para dar suporte à resposta; portanto, um comentário em vez de uma resposta.
Com relação a:
Os livros que eu sugeriria e usaria são:
Lógica em Ciência da Computação - Modelagem e Raciocínio sobre Sistemas 2nd Ed. por Huth e Ryan Isso introduz a lógica e passa para a verificação do modelo, mas não entra na prova do teorema. Portanto, isso deve cobrir todas as suas perguntas básicas relacionadas à verificação de lógica e modelo.
Princípios de verificação de modelo por Baier e Katoen Comecei a ler este, e é muito melhor do que ler muitos papéis e tentar ver como eles se encaixam. Esse é um dos livros mais recomendados, se não o mais recomendado, sobre o assunto de verificação de modelo. Ele deve responder às perguntas mais avançadas sobre verificação de modelo.
Lógica temporal e sistemas de estado de Kroger e Merz Costumo gostar de ter livros de diferentes autores quando aprendem sobre um assunto. Este é complementar / arredondar "Princípios de verificação de modelo"
Manual de lógica prática e raciocínio automatizado de Harrison Sendo um programador, não posso recomendar este livro o suficiente. O livro começa com a introdução da lógica e avança até o ponto de criar o kernel para um provador de teoremas baseado no trabalho de HOL Light . Apenas para destacar que o livro usa o código OCaml funcional, explica os teoremas em termos que considero amigáveis e fornece o que você precisa saber, mas não tanto que não consiga estabelecer a conexão ou sinta que está correndo pelos trilhos. Se é um livro muito focado em passar da lógica para um tipo específico de provador de teoremas.
Como provar isso: uma abordagem estruturada de Velleman Para entrar nos assistentes de prova para provar o teorema, você precisará viver e dormir com os teoremas.
Uma introdução às provas e ao vernáculo matemático diurno Este é um livro gratuito que não apenas complementa "Como provar isso", mas também o excede em suma. Eu não ficaria surpreso ao ver este se tornar popular.
No momento, não posso expandir mais a prova de teoremas, porque ainda estou aprendendo os prós e contras e as diferenças de cada um, mas os que estou focando são
Isabelle porque é baseada na unificação de ordem superior.
Esses assistentes de prova também costumam ter livros, são atuais, populares, de código aberto, mantidos e têm comunidades de suporte ativas.
Nota: usei worldcat.org para referenciar os livros, mas você pode revisá-los usando o recurso de visualização interna da Amazon.
fonte