Verificação 06/03/2012

   # # # # # # # # # # # # #
  # Verificação Automatica  #
  # Prof. Sérgio Campos     #
  # notasdogarcia.blog.com  #
   # # # # # # # # # # # # #

// Primeira aula teve uma explicação básica do que é a materia
// e teve vários exemplos onde erros na computação geraram problemas grandes.
// Básicamente a materia é sobre quais são os métodos seguros para se verificar erros de programação
// e como utiliza-los.

  Onde um erro pode estar escondido?
    - No Código
    - No Compilador
    - No SO
    - No Hardware

  O que pode ser feito para se verificar erros??
    Pode-se criar modelos matematicos que provem que ta tudo certo.

  O modelo que é criado é um modelo que defina o estado do programa e as relações de transição.

  Esse modelo pode então ser usado para fazer a prova.

  Uma prova dessas pode ser feita:
    - À mão
    - De forma semi-automatica
    - De forma totalmente automatica.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  Isso funciona? Mais ou menos

  E se o modelo estiver errado? Se voce perguntar algo que não é o que voce queria saber?

  Voce pode provar algo que não era o seu problema real.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  O problema de testes é que testando voce encontra erros comuns, erros que seriam fáceis de achar.

  O verificador automatico ele caminha testando todas as possibilidades possíveis e encontra erros incomuns,
  o problema disso é que o número de possibilidades é grande de mais para voce testar todas dessa forma.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  Hoje em dia essas verificações são feitas dividindo-se o código em várias sub-partes e testando-se cada uma separadamente.
  Assim o número de possibilidades de entradas não fica tão imenso.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  // No fim da decada de 60 já se preocupavam com isso, houve uma conferencia da OTAN a respeito da "Crise do Software"

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  Tripla de Hoare: P | S | Q

  Ela é dada pelos 3 elementos:
    - Pre-condição P.
    - Processo S.
    - Pós-condição Q.

  Ela é um modelo lógico que assume que se P é verdadeiro e S executou até o final então agora Q é verdadeiro.

  Essa idéia é importante porque voce pode analisar o código linha por linha, basta identificar os elementos de P e de Q.
  Isso é chamado de raciocinio composicional, ou seja voce divide os testes totais em vários pequenos testes.

// Nota Solta: Essa aula não tem prova. apenas projetos.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  Logica temporal e Reatividade de sistemas.

  Isso é uma coisa do tipo, se A || B então no futuro C vai acontecer.

  É uma variação da Tripla de Hoare, que funciona bem para algoritimos em paralelo onde voce não sabe bem quando algo vai acontecer, mas sabe que vai.
  // Voce não sabe quando porque voce não pode saber qual dos dois programas paralelos vai trabalhar primeiro, o que deixa tudo confuso.

  Essa lógica permite que voce pense sobre programas em paralelo.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  Model Checking
    1 - Especifique propriedades em logica temporal.
    2 - Construa um modelo de estado finito explicitamente. (ou seja liste todas as possibilidades)
    3 - Cheque se o modelo satisfaz a especificação para cada possibilidade.
    4 - Encontre contra exemplos quando o modelo tiver erros.

  É expressivo, composicional (baseado em Lógica Temporal) e portanto é eficiente e linear em relação ao tamanho do modelo.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  Verificação formal é tão importante hoje que é considerado essencial para muitas grandes empresas.

  Existem ainda empresas cujo o porduto é a verificação formal.

  É portanto um assunto sem o qual a computação atual não vai sobreviver.

  A ferramenta que utilizaremos no curso, é o NUSMV, o professor aconselhou-nos a pesquisar sobre com antecedencia se tivermos interesse.