Verificação 15/03/2012

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

  Model Checking

  Model checking consiste em uma construção de um modelo finito, ou seja sem variáveis reais.

  A checagem é aplicada por uma checagem exaustiva dos estados.

  A brincadeira então é tentar encontrar algoritimos eficientes para lidar com isso.

  There are two general aproachs:
  Tem duas aproximações:
    - Temporal Logic Model Checking.
    - Behavior Conformance Checking.

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

  Modelos de Computação:

  Estados de
  // arvore infinita expressa em uma finita =D

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

  Logica de arvore Computacional

  Existem os Path quantifier

    A - para todos os caminhos
    E - existe um caminho

  Vamos juntar isso com os F, e Gs que já estudamos na ultima aula.

  Assim temos:

  EF g: existe um caminho onde fatalmente se atinge g.

  AF g: diz que é inevitavel atingir g por qualquer caminho.

  EG g: Existe um caminho onde g é sempre verdade.

  AG g: para todos os caminhos g é verdade =].

  Note que cada propriedade dessa pode ser verdadeira ou não dependendo do estado que ela está.

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

  Exemplos:

  EF (started & !ready) existe um estado onde não se está pronto mas já começou? isso leva a erro.
  AG (req => AF ack) se uma requisição ocorrer ela será recebida?

  AG (AF device_enabled): enable está sempre presente
  AG (EF restart): restart pode ser alcançado de qualquer lugar.

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

  O problema do model checking é descobrir quais estados s stisfasem a formula f =]

  find all states of M that s |= f

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

  Behavior Conformance Checking

  O sistema e a especificação são modelados em grafos simples, E então compara-se os dois grafos para determinar se o o comportamento do sistema é de acordo com a especificação.

  Diferentes noções de Conformance:
    - Language inclusion
    - Refinement orderings
    - Observcational equivalence.

  Esses grafos podem ser muito simples ex:  (   ) ------> ( P )   esse grafo indica que inevitavelmente P será chamado.
                                             Loop interno

  ( R ) ---> (   ) ---------> ( ack ) denota que R implica em ack em algum momento.
           Loop interno

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

  Automato de Büchi:

  é uma tupla de 5:

  K um set de estados finitos.
  P0 € K é o estado inicial
  €€ é é um alfabeto finito.

  Aceitação da linguagem:

  Se o negócio chegar no estado de aceitação uma unica vez.

  // Infinitamente frequente é o negocio de voce ranformar as repetições infinitas em loops em um grafo finito, ao invez de um grafo infinito.

  // Esse tipo de verificação existe mas o professor usa é logica temporal ele não gosta mto desse modelo

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

  Vantagens do Model Checking:

    Provador de teoremas é um metodo do tipo:

      a=>b & a ==> b, então se voce estava em um estado que voce já tinha a e chega em um que a e b são verdade.

    É interessante, porque tudo o que é possível provar é provavél por ele.
    Mas não é muito eficiente e é dificil de usar.
    // Ele chega a parar e perguntar pro usuário o que fazer

    Model checking é totalmente automático e rápido.
    Voce consegue verificar corretude do seu sistema, mesmo antes de terminar a especificação. Assim isso é muito útiil.

    Então voce consegue fazer correções durante a fase de projeto!

    É muito bom em encontrar erros pouco comuns.

  Desvantagens:
    Explosão do grafo: O grafo é gigante.

  Outras tecnicas aleviam isso:

    BDDs // o professor conhece o cara que fez isso

    Abstração // retirar partes do sistema para torna-lo mais simples
    Raciocinio Composicional // Divida o problema em subproblemas menores e resolva.
    Symmetry
    Ordem parcial
    Minimização semantica

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

  Já se pode verificar ate 10¹²⁰ estados, então essencialmente é um número infinito de estados.

  // Curiosamente: em um mesmo barramento pode-se colocar no máximo uns 4 processadores. Senão ia dar muito conflito.

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

  Seguiram-se exemplos de erros encontrados por model checking

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

  EMC CAESAR os primeiros

  SMV o primeiro a usar BDD

  Spin usa partial order reduction para evitar a explosão de estados.

  Mur<phi> são baseado no Unity programming

  E outros.

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

  // Fim da aula =]