Introdução

Um protocolo pode ser entendido como um conjunto de regras para interação de processos concorrentes. Um aspecto essencial de um protocolo é o conjunto de sequências de mensagens e ações permitidas. Por exemplo, no protocolo de enlace PTP as sequências a seguir são aceitáveis (prefixo C: identifica uma ponta do enlace, e S: a outra ponta):

C:DATA_0, S:ACK_0, C:DATA_1, S:ACK_1
C:DATA_0, S:ACK_0, S:DATA_0, C:ACK_0, C:DATA_1, C:DATA_1, S:ACK_1

... mas estas não:

C:DATA_0, S:ACK_1, C:DATA_1, S:ACK_0
C:DATA_0, S:DATA_0, C:ACK_0, S:ACK_0

As regras de procedimento devem manter sempre o estado do protocolo consistente em todas as entidades de protocolo envolvidas (no exemplo, tanto no cliente quanto no servidor). Isso não é simples de garantir, mesmo com protocolos de baixa complexidade. Tome-se o exemplo de um protocolo para transferência de sequências de caracteres por linhas analógicas, descrito na seção 2.3 do capítulo 2 do livro Design and Validation of Computer Protocols, chamado de protocolo Lynch.

O propósito do protocolo Lynch é transferir arquivos de texto como sequências de caracteres através e uma linha telefônica, com proteção contra erros, supondo que todos erros de transmissão possam ser detectados. Comunicações são full-duplex, e confirmações positivas e negativas são empregadas para implementar um mecanismo de garantia de entrega de mensagens. Cada mensagem possui duas partes: o dado transmitido e informações de controle que se aplica às transmissões em sentido reverso. Supõe-se que mensagens possam ser distorcidas, mas não perdidas, inseridas, duplicadas ou reordenadas, e que exista um módulo de mais baixo nível (ex: encoder/decoder) que transforme uma mensagem distorcida em uma mensagem especial do tipo err. O vocabulário do protocolo é formado por três mensagens:

ack: composta por um dado e uma confirmação positiva do dado recebido previamente em sentido contrário.
nak: composta por um dado e uma confirmação negativa do dado recebido previamente em sentido contrário.
err: mensagem especial que representa uma mensagem recebida com erro.

As regras de procedimento desse protocolo são:

Se a recepção anterior foi livre de erros, a próxima mensagem no canal reverso deve incluir uma confirmação positiva. Se a recepção anterior possuir erro, deve-se incluir uma confirmação negativa.
Se a recepção anterior incluir uma confirmação negativa, ou a recepção anterior possuir erro, deve-se retransmitir a mensagem no canal reverso. Caso contrário, obtém-se uma nova mensagem para transmissão

Essas regras podem ser representadas por diferentes tipos de diagramas, dentre eles este diagrama SDL:

Diagrama SDL para o protocolo Lynch

Como se pode verificar se esse protocolo funciona a contento ? Em outras palavras, que ele possibilite a comunicação livre de erros entre duas entidades ? Antes de mais nada, deve-se definir o que se entende por funcionar a contento. No caso do protocolo Lynch, seu correto funcionamento pode ser expresso por estas propriedades:

Garantia de entrega: toda mensagem enviada por uma entidade do protocolo no final das contas é recebida pela outra entidade do protocolo.
Duplicatas descartadas: Mensagens duplicadas não são aceitas

Parece simples verificar se essas propriedades sempre valem a longo da operação do protocolo. O protocolo é de baixa complexidade, e isso aparentemente deve ser fácil de conferir.

Atividade

Verifique se as propriedades do protocolo Lynch sempre valem ...

Modelos para verificação

A verificação de propriedades de um protocolo envolve demonstrar que suas propriedades desejadas nunca são violadas. Existem diferentes técnicas para realizar esse tipo de verificação, tais como álgebra de processos, verificação de modelos e até mesmo simulação (se bem que esta última não é capaz de fornecer um veredito definitivo). Nesta disciplina será estudada a verificação de modelos, ou model checking, como é mais conhecida.

A verificação de modelos envolve a criação de um modelo que represente o sistema a ser verificado, a identificação de propriedades desejadas expressadas de acordo com esse modelo, e a busca automática e exaustiva por violações dessas propriedades. Assim, três elementos estão envolvidos:

Um modelo do comportamento do sistema, expressado segundo algum formalismo: tratando-se de um sistema a eventos discretos, um protocolo pode ser modelado de acordo com alguma construção matemática para sistemas de estados finitos. Máquinas de estados finitos se aplicam a essa necessidade, porém alguns incrementos em relação às máquinas de estados vistas anteriormente são necessários. Em particular, o modelo do sistema em que se aplica um protocolo envolve duas ou mais máquinas de estados que se comunicam. Isso pode ser descrito implicitamente por alguma linguagem de programação de propósito específico.
Um conjunto de propriedades desejadas do sistema: as propriedades correspondem a combinações de condições baseadas em atributos do modelo, ou sequências de eventos.
Uma ferramenta que automatize a busca exaustiva de violações de propriedades dentro do modelo: tal ferramenta deve explorar todas as possíveis sequências de eventos no modelo, verificando as propriedades desejadas a cada passo.

Para introduzir a verificação de modelos, um exercício sobre o protocolo Lynch será realizado. Mas antes é necessário conhecer uma linguagem de modelagem para verificação de sistemas e uma ferramenta de verificação que se baseie nessa linguagem.

A linguagem PROMELA e o verificador SPIN

A linguagem PROMELA (Process Meta-Language), conforme introduzida no capítulo 2 e melhor descrita no capítulo 3 do livro The SPIN Model Checker (PDF), é uma linguagem para modelagem de sincronização e coordenação de processos concorrentes. Sendo voltada para verificação de sistemas, essa linguagem não se aplica a expressar algoritmos em geral, tampouco calcular coisas. Seus elementos básicos são:

Processos assíncronos
Canais de mensagens bufferizados ou não
Declarações de sincronização
Dados estruturados

Intencionalmente não há noção de tempo, não existe um relógio a ser consultado, não existem números em ponto flutuante e há poucas funções computáveis. Esse desenho enxuto torna a modelagem de sistemas concorrentes relativamente simples com essa linguagem (ao menos essa é a intenção). A execução e verificação de programas escritos em PROMELA se faz com um verificador de modelos chamado SPIN (Simple PROMELA Interpreter). Essa ferramenta possibilita executar modelos de forma a simulá-los ou a verificá-los exaustivamente.

A modelagem de sistemas envolve portanto a escrita de programas em PROMELA. Assim, a seguir se apresenta uma introdução sobre a linguagem com base em seus elementos básicos.

Uma versão precompilada do spin está disponível em um servidor do Ifsc:

spin

É suficiente baixá-la para seu computador, e então lhe dar permissão de execução com este comando:

chmod +x spin

Caso prefira, a versão precompilada do Spin do site oficial é esta (ela pode ser mais atual do que a mantida aqui no Ifsc):

Versão precompilada

Escolha a versão apropriada para o seu sistema operacional, e descompacte-a. Curiosamente o programa precompilada está compactado duas vezes com gzip, e é mais fácil descompactá-lo via linha de comando. Por exemplo:

gunzip spin648_linux64.gz
gunzip -c spin648_linux64 > spin

De forma alternativa, pode-se instalar o SPIN a partir de seu código-fonte:

Instale os softwares bison e flex. No Ubuntu ou Debian isso se faz assim:
```
sudo apt-get install bison flex
```
Obtenha o código-fonte do SPIN
Descompacte-o em algum diretório
A partir desse diretório, em um terminal entre em Spin/Src6.4.3
Execute o comando make
Ao final, o programa spin deve ter sido compilado.

Processos assíncronos

Um processo é declarado com a palavra-chave proctype, seguida de seu nome. O processo abaixo apresenta o famigerado hello world na saída padrão e em seguida termina.

active proctype hello() {
  printf("hello world: meu id é %d\n", _pid)
}

Para executá-lo, salve-o em um arquivo e em seguida execute-o usando o spin. Por exemplo, se o nome do arquivo que o contém for hello.pml, a execução com spin deve ser assim:

aluno@M2:~$ spin hello.pml
hello world: meu id é 0
1 process created

A palavra-chave active define que o processo deve ser executado assim que o programa iniciar. Uma vez terminado, a execução como um todo encerra, uma vez que nenhum processo permanceceu ativo. Um outro exemplo gera processos indefinidamente, e mostra como se pode iniciar um processo a partir de outro usando o comando run:

active proctype hello() {
  printf("hello world: meu id é %d\n", _pid)
  run hello()
}

Variáveis

Processos podem usar variáveis, cujos escopos podem ser locais ou globais. Variáveis são tipadas, e os tipos básicos são :

bit
bool
byte
chan
mtype
pid
short
int
unsigned

OBS: mais detalhes ver capítulo 3 do livro The SPIN Model Checker

A declaração de variáveis é semelhante à de linguagem C, como se pode observar neste exemplo:

mtype = {ack, nak, err}

active proctype hello() {
  int x;
  pid p;
  mtype m = ack

  p = _pid;
  x = x + 1;
  printf("hello world: meu id é %d e x=%d\n", p, x)
  printf("... e m=")
  printm(m)
  printf("\n")
}

Tipos definidos

Podem-se definir tipos de dados de forma semelhante à declaração struct de linguagem C, usando-se a palavra-chave typedef:

typedef Mensagem {
  byte cod;
  int uid
}

active proctype teste() {
  Mensagem msg

  msg.cod = 111
  msg.uid = _pid
  printf("Mensagem: %d, %d\n", msg.cod, msg.uid)
}

.. o que pode ser conveniente para representar mensagens de um protocolo.

Canais de mensagens

Canais de mensagens são usados para modelar a troca de dados entre processos, e podem ser locais ou globais. Cada canal é declarado de forma a possibilitar mensagens de acordo de um determinado tipo, como neste exemplo:

typedef Mensagem = {
  pid uid;
  int cod
}

chan canal = [1] of {int}
chan outro = [8] of {Mensagem}
chan maisum = [0] of {int, byte}

No trecho de programa acima, são declarados três canais:

canal: este canal transporta mensagens com do tipo int; ele possui uma fila com até 1 mensagem armazenada (enviada e ainda não recebida)
outro: este canal transporta mensagens do tipo Mensagem, e possui uma fila com até 8 mensagens
maisum: este canal transporta mensagens compostas por dois campos (int e byte), e não possui fila de mensagens. A ausência de fila implica a comunicação síncrona de processos: o transmissor bloqueia até que o receptor receba a mensagem

A comunicação por meio de um canal se faz com os comandos ! (envio) e ? (recepção), que devem ser usados desta forma:

chan canal1 = [1] of {int}
chan canal2 = [1] of {int, byte}

active proctype p1() {
  int msg
  byte codigo

  // envia uma mensagem pelo canal1
  canal1!9

  // aguarda uma mensagem pelo canal2
  canal2?msg,codigo

  printf("Recebeu %d,%d\n", msg, codigo)
}


active proctype p2() {
  int msg

  // envia uma mensagem pelo canal2
  canal2!2,15

  // aguarda uma mensagem pelo canal1
  canal1?msg

  printf("Recebeu %d\n", msg)
}

O envio é feito informando-se valores para cada campo do tipo de mensagem transportada pelo canal. Esses valores podem ser constantes ou fornecidos por variáveis. O envio não é bloqueante se houver espaço livre na fila do canal para mais uma mensagem. Se o canal estiver cheio, o envio causa o bloqueio do transmissor, mas isso pode ser mudado no Spin (ver seção sobre Message Channels do capítulo 3 do livro sobre o Spin). A recepção é sempre bloqueante, e segue uma sintaxe similar a da operação de envio. Logo após o comando e recepção ?, podem-se informar variáveis para armazenar o conteúdo da mensagem, ou especificar constantes. No segundo caso, a recepção somente é realizada se os valores das constantes forem iguais aos da mensagem a ser recebida através do canal.

Um exemplo simples e representativo é este modelo de um protocolo de bit alternado. Ele é composto por um processo transmissor e um receptor, os quais repetem indefinidamente uma sequência de mensagens. As mensagens se dividem em dados (msg0 e msg1) e confirmação (ack0 e ack1). O programa PROMELA para esse protocolo está a seguir:

mtype = { msg0, msg1, ack0, ack1 };
chan    to_sndr = [2] of { mtype };
chan    to_rcvr = [2] of { mtype };

active proctype Sender()
{
again:  to_rcvr!msg1;
        to_sndr?ack1;
        to_rcvr!msg0;
        to_sndr?ack0;
        goto again
}

active proctype Receiver()
{
again:  to_rcvr?msg1;
        to_sndr!ack1;
        to_rcvr?msg0;
        to_sndr!ack0;
        goto again
}

Executabilidade

Em PROMELA, uma sentença é executável ou não (bloqueável). A semântica de executabilidade de sentenças em PROMELA segue estas regras:

atribuições e comandos do tipo print são sempre executáveis. Em outras palavras, nunca bloqueiam.
envio de mensagens é executável se o canal não estiver cheio, do contrário é bloqueante
recepção de mensagens é executável se houver mensagem no canal E se os valores nela contidos foram consistentes com os valores porventura especificados no comando de recepção
expressões são executáveis se avaliarem para verdadeiro (true)

PROMELA define também um modelo de execução não-determinístico. Isso quer dizer que, se uma sequência apresentar uma bifurcação e ambos os ramos forem executáveis, um deles será sorteado para ser executado. Por exemplo:

chan canal1 = [1] of {int}
chan canal2 = [1] of {int}

active proctype p1() {
  int msg1, msg2

Repetir:

  if
  :: canal1?msg1 -> printf("Recebeu msg1=%d\n", msg1)
  :: canal2?msg2 -> printf("Recebeu msg2=%d\n", msg2)
  fi

  goto Repetir
}

active proctype p2() {
  denovo:

  if
  :: canal1!111
  :: canal2!222
  fi
  
  goto denovo
}

No processo p2 do exemplo acima, se somente canal1 tiver uma mensagem, a primeira sentença será executada. Se somente canal2 tiver uma mensagem, a segunda sentença será executada. E se ambos canais tiverem mensagens, qualquer uma das duas sentenças poderá ser executada. E o processo p1, por sua vez, fica indefinidamente enviando mensagens por ambos canais aleatoriamente.

Na estrutura de seleção if, uma sentença especial é dada pela palavra-chave else. Tal sentença é executável somente se nenhuma outra sentença do if for executável.

Repetição

O exemplo do processos transmissor p2 na seção anterior envolveu a repetição de transmissões pelos canais canal1 e canal2. A repetição foi controlada com o comando goto. Em PROMELA existe um comando específico para controlar a repetição. Ele possibilita reescrever o processo p2 daquele exemplo para que fique assim:

active proctype p2() {
  do
  :: canal1!111 -> printf("enviei pelo canal1\n")
  :: canal2!222 -> printf("enviei pelo canal2\n")
  od
}

Da mesma forma que a estrutura de seleção if, a estrutura de repetição do seleciona uma das sentenças executáveis de forma não-determinística. Se nenhuma sentença for executável, então do bloqueia. E, assim como no if, a sentença iniciada com else é executável se nenhuma outra sentença do mesmo bloco de repetição for executável. Por fim, o comando break possibilita interromper a repetição. O exemplo a seguir combina else e break: se não for possível enviar uma mensagem pelo canal1, tampouco pelo canal2, então a repetição é interrompida.

active proctype p2() {
  do
  :: canal1!111 -> printf("enviei pelo canal1\n")
  :: canal2!222 -> printf("enviei pelo canal2\n")
  :: else -> break
  od
}

Outra palavra-chave importante de PROMELA é timeout, cujo significado se assemelha a else. A diferença está no escopo: else é verdadeiro se nenhuma condição do bloco em questão for executável, e timeout é verdadeiro se nenhuma sentença de todos os processos do programa for executável.

Além de do .. od, pode-se usar for para repetir um bloco de sentenças com base em uma faixa de valores.

active proctype p2() {
  int x

  // envia 10 mensagens por canal1 ou canal2,
  // selecionando-os de forma não-determinística
  // os limites da faixa de valores podem ser expressões contendo
  // constantes ou variáveis
  for (x: 1..10) {
    if
    :: canal1!x -> printf("enviei %d pelo canal1\n", x)
    :: canal2!x -> printf("enviei %d pelo canal2\n", x)
    fi
  }
}

Seleção de valores

A seleção ou sorteio de valores pode ser feita com select, que escolhe um valor dentre uma faixa:

proctype teste() {
  int x = 0

  // seleciona um valor entre 1 e 20 e armazena-o em x
  // sai do laço quando x >= 10
  // os limites da faixa devem se expressões contendo somente constantes
  do
  :: x < 10 -> select(x : 1 .. 20)
     printf("%d -> x=%d\n", _pid, x)
  :: else -> break
  od
}

Modelagem de Máquinas de Estados Finitos

Máquinas de estado finitos são facilmente modeladas com Promela, explorando-se rótulos e a estrutura de repetição do .. od. Por exemplo, seja a MEF a seguir:

Essa MEF pode ser traduzida para um modelo Promela como este. Note cada estado representado por do .. od e prefixado por um rótulo. As expressões sentinelas do do .. od correspondem aos gatilhos das transições que saem daquele estado, e as ações correspondentes representam o que acontece se a transição for disparada. Por fim, a mudança de estado é realizada por um simples goto para o rótulo do próximo estado.

active proctype mef() {
  int x 

  estado0:
  do
  :: x < 10 ->
    x++
  :: x == 10 ->
    goto estado1
  od

  estado1:
  do
  :: x > 0 ->
    x--
  :: x == 0 ->
    goto estado0
  od
}

Atividade

Escreva um modelo para o problema do produtor e consumidor. Suponha que o produtor produza 10 mensagens e depois termine, e o buffer intermediário tenha capacidade para 4 mensagens.
Modifique seu modelo da questão anterior para que existam 2 produtores.
Escreva um modelo para um protocolo do tipo pare-e-espere em um ambiente de execução livre de erros.
Escreva um modelo para um protocolo do tipo pare-e-espere em um ambiente de execução em que erros são possíveis ... seu modelo deve prever a perda de mensagens, retransmissões e descarte de mensagens duplicadas.
Crie um modelo para o protocolo Lynch e use-o para verificar se esse protocolo é livre de erros.
Escreva um modelo para o enquadramento que foi implementado no protocolo ponto-a-ponto.

Modelos para o protocolo pare-espere
Modelos implementam esta MEF

PTC29008: Verificação de Protocolos

Índice

Introdução

Atividade

Modelos para verificação

A linguagem PROMELA e o verificador SPIN

Processos assíncronos

Variáveis

Tipos definidos

Canais de mensagens

Executabilidade

Repetição

Seleção de valores

Modelagem de Máquinas de Estados Finitos

Atividade

Menu de navegação

Pesquisa