Verificação Formal de Software
Uma Introdução Informal
Professor Alair Dias Júnior
- Verificação sem testes (dinâmicos)
- Isso é possível?
- Sim! É possível!
- Conceitos
- Verificação sem testes (dinâmicos)
- Verificação Formal
- Considerações Finais
Conceitos e Motivação
- Verificação: processo de se determinar se um sistema atende ou não a uma especificação.
- Validação: processo de se determinar se um sistema atende às necessidades do usuário.
- Teste (dinâmico): processo de se executar o sistema aplicando-se valores de entradas e, então, observar e analisar os resultados.
- Quantas combinações devem ser testadas?
- Depende dos tipos de entrada
- Depende da memória do sistema
- Pontos fortes
- Intuitivo
- Largamente utilizado
- Escalável
- Pode ser caixa-preta ou caixa-branca
- Pontos fracos
- Ineficiente
- Controlabilidade complicada
- Incompleto, exceto nos programas mais triviais
Verificação sem Testes (dinâmicos)
- Exemplos
- Inspeção de Código
- IDE/Compilador
- Análise Léxica
- Análise Sintática
- Análise Semântica
- Teoria de compiladores
- Sim! FTC e compiladores servem também para quem não contribui para o GCC!
| Característica | Estática | Dinâmica |
| Caixa-branca | ||
| Caixa-preta | ||
| Completude | ||
| Resultado Parcial |
Verificação Formal
- Baseada em análise estática de código
- Model Checking
- Equivalence Checking
- P1, P2, P3 são propriedades
- E é a Especificação do Sistema
- Model-checking não requer uma especificação total do sistema
- Trabalha sobre um conjunto de especificações parciais
- Mais fácil de criar, manter e verificar
- Um asserção da propriedade é uma afirmação de que o sistema possui aquela propriedade
- Uma asserção válida é uma asserção que é verdadeira para qualquer estado do sistema
- Existem várias formas de escrever asserções
- Linguagens com capacidade de expressão lógica e temporal
- Problemas de alcançabilidade
(x > 0) \wedge (y > 0) \rightarrow (z > 0)
(x \lt 0) \wedge (y \lt 0) \rightarrow (z \lt 0)
- Algumas vezes é impossível determinar o limite superior de um laço
- Ou o tempo para chegar ao limite superior seria muito alto
- Pode-se limitar o número de passos ou iterações que serão executadas
- Filtros digitais projetados usando ponto-flutuante e implementados usando ponto-fixo
- Arredondamentos e erros acumulados podem levar a instabilidades
- Exemplo: um filtro IIR com precisão de 7 bits (Q2.5)
- Das 1200 bilhões de sequências, somente 26 apresentam erros
- 30 minutos de testes aleatórios e testes dirigidos não conseguiram encontrar contraexemplos
- BMC apresenta um contraexemplo em menos de 1 minuto
Considerações Finais
- É possível aplicar verificação formal no mundo real?
- Sim! As ferramentas são bem maduras já.
- Mas os resultados não são intuitivos
- É necessário um período de adaptação
- O tamanho do sistema é um problema
- A memória pode ser insuficiente
- Testes de unidades e partes críticas podem se beneficiar
- As asserções podem ser usadas em testes dinâmicos!
- VF tem sido muito utilizada em projeto de circuitos integrados
- Erros costumam ser mais caros que no caso de software
- Verificação de programa de CLPs
- Verificação Semi-formal
- Priorização de casos usando Heurísticas