PTC29008: Verificação de Protocolos: Lógica temporal
- Manual LTL para Spin
- Introdução a LTL no Spin
- Métodos formais e Lógica Temporal
- Resumo sobre Spin e LTL
Lógica clássica é boa para descrever um mundo estático, mas sistemas computacionais são dinâmicos. A lógica temporal é uma categoria de formalismos que procura descrever como as propriedades de um sistema variam com o tempo, porém sem se referir explicitamente ao tempo. As propriedades que tipicamente são verificadas com lógica temporal são:
- Segurança (safety): nada de ruim irá acontecer. Ex: não há deadlock, não ocorrem violações de exclusão mútua, mensagens duplicadas não são entregues.
- Vivacidade (liveness): algo de bom vai ocorrer. Ex: um programa fatalmente irá terminar, uma mensagem transmitida será corretamente recebida em algum momento futuro.
- Justiça (fairness): sistemas independentes progridem. Ex: se o meio de transmissão estiver frequentemente disponível, uma entidade de protocolo no final das contas conseguirá transmitir uma mensagem.
A lógica temporal introduz operadores temporais, usados para descrever a dinâmica de sistemas ao longo do tempo. Curiosamente, o tempo não aparece explicitamente em expressões formadas com esses operadores. Para fins de nosso estudo, será considerado um tempo linear, com um único caminho de execução (a alternativa é um tempo ramificado, em que múltiplos caminhos de execução são levados em conta). Ambas abordagens pressupõem um sistema modelado como um sistema de transições com rótulos (LTS - labeled transition system), como, por exemplo, máquinas de estados finitos. Cada passo de um caminho de execução é definido por um conjunto de proposições primitivas que avaliam para verdadeiro. Exemplos de proposições são:
- msg_tx: mensagem foi transmitida
- inCS_A: processo A está executando em uma seção crítica
- x == 0: variável x tem valor 0
- proc@label: processo proc está executando linha identificada pelo rótulo label
Sendo assim, um estado S é definido pelas proposições que são verdadeiras nesse estado.
Operadores temporais
Os operadores temporais se aplicam a estados, considerando uma sequência de estados. Tomando-se as fórmulas de lógica temporal f e g:
- Xf: f é verdadeiro no próximo estado (next f)
- Gf: f é verdadeiro em todos os estados (always f)
- Ff: f é verdadeiro em algum estado futuro (eventually f)
- fUg: g é verdadeiro em algum estado futuro, e f é verdadeiro em cada estado até então (f until g)
Outra notação:
- G:
- F:
- X:
Dado o conjunto de proposições P, e fórmulas LTL f e g, as fórmulas LTL podem ser formadas com estas regras:
- p (uma proposição )
- Operadores booleanos:
- : not f
- : f or g
- : f and g
- : f implies g
- Operadores temporais:
- f U g
Uma outra forma de visualizar esses operadores temporais está ilustrada a seguir:
Algumas identidades entre fórmulas com esses operadores são:
- ...
- ,
- ,
- f W g
Propriedades distributivas:
LTL e Spin
O verificador spin é capaz de verificar fórmulas LTL. As proposições primitivas podem ser:
Proposição primitiva | Exemplo |
---|---|
expressões baseadas em variáveis globais | (x == 0) |
rótulos de processos | p1@inicio (rótulo inicio do processo p1) p1[2]@inicio (rótulo inicio do processo p1 com pid 2) |
variáveis locais de processos | p1:x (variável local x do processo p1) p1[2]:x (variável local x do processo p1 com pid 2) |
Os operadores temporais suportados são (OBS: note a falta do operador next):
Operador LTL no Spin | Operador LTL |
---|---|
[] | (always) |
<> | (eventually) |
U | U (until) |
&& | |
|| | |
-> | |
<-> |
Variáveis e funções predefinidas que podem ser úteis:
- _pid: variável local que contém o PID de um processo
- _last: variável global que contém o PID do processo que contém a última sentença executada
- enabled(pid): função global que retorna true se existe ao menos uma sentença executável no processo identificado por pid
Para declarar fórmulas LTL em um modelo Promela, basta acrescentá-las ao final do arquivo com esta sintaxe:
ltl nome1 { formula 1}
ltl nome2 { formula 2}
...
ltl nomeN { formula N}
A geração do verificador deve ser feita com estes comandos:
spin -a modelo.pml
gcc -o pan pan.c
Por fim, a execução do verificador se faz assim:
./pan -a
Exemplo de uso
Um primeiro exemplo pode ser aplicado ao caso de exclusão mútua entre processos. Supondo que inCS_X signifique processo X está na seção crítica, as seguintes proposições podem ser definidas:
- Processos A e B nunca estão na seção crítica ao mesmo tempo:
- Nenhum dos processos monopoliza a seção crítica:
No spin, essa verificação pode ser feita com este modelo e respectivas fórmulas LTL:
mtype { p, v };
chan sema = [0] of { mtype };
active proctype Dijkstra()
{ byte count = 1;
end: do
:: (count == 1) ->
sema!p; count = 0
:: (count == 0) ->
sema?v; count = 1
od
}
active proctype p1()
{ do
:: sema?p; /* enter */
critical: skip; /* leave */
sema!v;
od
}
active proctype p2()
{ do
:: sema?p; /* enter */
critical: skip; /* leave */
sema!v;
od
}
// Apenas um processo está em sua seção crítica por vez
ltl crit { [] (! p1@critical || ! p2@critical)}
// Nenhum processo monopoliza a seção crítica
ltl justica { [] (p1@critical -> <> ! p1@critical) && [] (p2@critical -> <> ! p2@critical)}
Atividades
1. Para o sistema descrito no modelo Promela a seguir, verifique se o contador atinge o valor 10:
int count;
bool incr;
active proctype counter() {
do
:: incr -> count++
od
}
active proctype env() {
do
:: incr = false
:: incr = true
od
}
Fórmula LTL |
---|
2. Para o sistema do exercício 1, verifique também se a execução dos processos possui a propriedade da justiça: ambos os processos devem executar infinitamente frequente. Dica: lembre das variáveis e funções predefinidas do Spin.
Fórmulas LTL |
---|
3. Seja um protocolo ARQ do tipo pare-espere, em que processo p1 envia mensagens para processo p2 por um canal não confiável:
- Defina sentA para expressar se processo p1 recém enviou mensagem A, e recA se processo p2 recém recebeu mensagem A. Defina também sentB e recB da mesma forma.
- Defina loss para expressar se canal perdeu última mensagem
Sendo assim, verifique estas propriedades:
- Se uma mensagem for transmitida, ela será recebida em algum momento
- Se uma mensagem for recebida, ela foi previamente transmitida
Por fim, escreva esse modelo Promela, declare as fórmulas LTL, e verifique seu modelo.
4. Aplique a verificação com LTL aos problemas propostos aula passada ...