Verificação 13/03/2012

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

Sistemas reativos são aqueles em que voce não produz o resultado e ele não termina.
Ou seja seu processamento é em reação às entradas do ambiente.

Um exemplo de sistema de menssagens entre computadores
O sistema usa um contador de sequencia para garantir a coesão das menssagens.

O que podemos afirmar?

  - toda menssagem é recebida
  - Uma menssagem não é recebida sem ser enviada.
  Se x é enviado antes de y então é recebido antes de y.

  Sender continues resending the menssage until lack
  if channel continues do receive input it eventualy transmits does not drop a msg rcv does not ack before msg is output.

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

  Assim podemos dizer:

  para todo t> 0: input (x,t) -> €t'>= t: output (x,t')

  Mas isso é complicado.

  Em logica temporal temos a variável G (global)
  G p é valido se a variável p será verdadeira daqui pra frente para todo instante t > t0.

  F p é verdade se em algum momento no futuro p necessariamente será verdade.

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

  Note que G e F são duais:
  G p == !F !p
  F p == !G !p

  G p && G q == G(p && q)
  F p || F q == F(p || q)

  Mas note:

  G p || G q != G(p || q)
  F p && F q != F(p && q)

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

  Nosso exemplo anterior (complicado) pode ser re-escrito assim:

  G(input(x) ==> output(x))

  E pode ser transcrito assim: É globalmente verdade que se há um input havera um output.

  // Note que esse modelo pode ser alterado para se adequar melhor ao seu problema.

  O professor chamou esse exemplo acima de propriedade de Vida ou de "Liveness"

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

COMENTARIO Solto:
   (HT && !HT)==>LQ
   HT = hoje é terça, LQ = lua é feita de queijo =D. E isso é verdade já que uma coisa falsa pode implicar em qualquer outra coisa falsa.

   Cuidado com isso, uma premissa falsa implicando em qualquer outra coisa não quer dizer que a implicação seja falsa, apenas a premissa, já que ela nunca ocorre a implicação também não, então é verdade para todos casos =P.

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

  Propriedades infinitamente frequentes:

  G F p significa que algo certamente acontecerá no futuro.

  G F send(x) ==> G F recv(x)
  // Esse é o tipo de propriedade de justiça (fairness)

  Se um sistema sempre reinicia (não entra em loop) então:
  G F restart

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

  O operador "Até" (Until) p U q.

  Assim p é verdade até que q seja verdade.

  Essa propriedade é interessante em outro sentido. q necessárimente deve acontecer.
  Se q não acontecer no futuro, p U q não é verdade também.

 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

  O operador "Até" fraco:
  p W q == p U q || G p

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

  Uma propriedade de fairness ou safety pode ser provada falsa em uma execução finita.

  Em uma propriedade de liveness ou de vida voce precisa rodar por um tempo infinito para provar que é falso.
  // Na prática nesse tipo de propriedade voce caminha até encontrar um ciclo, se encontrar e ele ainda for falso, ==> é falso.

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

  O operador de próximo tempo: X p é verdade em um momento se no próximo instante p é verdade. no instante t + 1

  Past time operators: H, P e S são os equivalentes ao passado de: G, F e U.
  // Mas quase ninguém usa isso.

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

  Ferramenta:
  Nu SMV: a New Symbolic Model checker

  Site: http://nusmv.fbk.eu/
  // Software de aluno de pós-graduação:
  // É um software que funciona, na mão do cara =P
  // Mas um grupo italiano comprou ele e deixou isso mais simples e completo =], então podemos usar.

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

  Exemplo da linguagem do NuSMV:

  MODULE main

  VAR

  state1: (n1, t1, c1);
  // n1, não no estado critico
  // t1 tentando entrar no critico.
  // c1 no critico.

  ASSIGN

  init(state1 := n1;

  next(state1) :=
  case
    (state2 == n1) & (state2 = t2): t1;
    (state2 == n1) & (state2 = n2): t1;
    (state2 == n1) & (state2 = c2): t1;
    (state2 == t1) & (state2 = n2): c1;
    (state2 == t1) & (state2 = t2) & turn = 1: c1;
    (state1 = c1): n1;
    TRUE : state1;
  esac;

  turn é a variável de "quem é a vez?"
  Assim se ambos competirem eles sabem quem vence.

  O que ele faz é um diagrama de estados.
  Assim para cada condição ele descobre um jeito de seguir.
  E se nenhuma condição ocorrer ele pode ficar no stado atual.

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

  Assim voce pode fazer as perguntas ao programa:

SPEC
  EF ((state = c1) & (state 2 = c2))
  // existe uma violação da exclusão mutua?

  E ele te retorna o resultado, com contra exemplos e etc.

  Usar ele é uma experiencia muito unica.

  No caso do EF acima ele retorna:

  -- specification EF (state 1 = c1 &* state 2 = c2) is false
  -- created by the following execution sequence
  Trace Description: CTL Couterexample
  Trace Type: Counterexample
  -> State: 1.1 //Algo assim essa parte de baixo eu copiei de outro exemplo então nõa deve ser coerente.
  state1 = n1
  state2 = n2
  turn = 1

  Mas nesse tipo de pergunta onde ele responde que nada acontece, normalmente a resposta não faz tanto sentido, já que para uma prova concreta ele teria que
  imprimir todos os caminhos possíveis, ele prefere nem tentar imprimir todos.

 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

  // comentários são feitos com "--"

  // Essa foi só uma passada rapida nós veremos isso com mais detalhes no futuro.

  // Note que geralmente testamos programas concorrentes, pois eles são mais interessantes.

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

  // Fim da aula.