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: $\square$
F: $\diamondsuit$
X: $\bigcirc$

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 $p\in P$ )
Operadores booleanos:
- $\neg f$ : not f
- $f\vee g$ : f or g
- $f\wedge g$ : f and g
- $f\implies g$ : f implies g
Operadores temporais:
- $\bigcirc f$
- $\square f$
- $\diamondsuit f$
- 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:

$\square f\Leftrightarrow \neg (\diamondsuit \neg f)$ ... $\diamondsuit f\Leftrightarrow \neg (\square \neg f)$
$\square \square f\Leftrightarrow \square f$ , $\diamondsuit \diamondsuit f\Leftrightarrow \diamondsuit f$
$\diamondsuit f\Leftrightarrow trueUf$ , $\square f\Leftrightarrow \neg (trueU\neg f)$
f W g $\Leftrightarrow fUg\vee f$

Propriedades distributivas:

$\square (f\wedge g)\Leftrightarrow \square f\wedge \square g$
$\diamondsuit (f\vee g)\Leftrightarrow \diamondsuit f\vee \diamondsuit g$
$\bigcirc (fUg)\Leftrightarrow (\bigcirc f)U(\bigcirc g)$
$\bigcirc (f\vee g)\Leftrightarrow (\bigcirc f)\vee (\bigcirc g)$
$\bigcirc (f\wedge g)\Leftrightarrow (\bigcirc f)\wedge (\bigcirc g)$

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
[]	$\square$ (always)
<>	$\diamondsuit$ (eventually)
U	U (until)
&&	$\wedge$
\|\|	$\vee$
->	$\implies$
<->	$\Leftrightarrow$

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:
- $\square (\neg inCS_{A}\vee \neg inCS_{B})$
Nenhum dos processos monopoliza a seção crítica:
- $\square (inCS_{A}\implies \diamondsuit \neg inCS_{A})$
- $\square (inCS_{B}\implies \diamondsuit \neg inCS_{B})$

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 ...

PTC29008: Verificação de Protocolos: Lógica temporal

Índice

Operadores temporais

LTL e Spin

Exemplo de uso

Atividades

Menu de navegação

Pesquisa