Redes de Petri Modelo de Especificação Formal Alessandra Guaracy de Oliveira Patrick Henrique da...

Redes de Petri

Modelo de Especificação Formal

Alessandra Guaracy de Oliveira

Patrick Henrique da Silva Brito

Sumário

Introdução Variantes de Redes de PetriFerramentas disponíveisEstudo de Caso (Elevador)Conclusões

Referências BibliográficasMaciel, Lins e Cunha. Introdução às Redes de Petri, 10ª Escola de Computação, 1996

Petri Nets Tool Database -http://www.daimi.au.dk/PetriNets/tools/db.html

Barros, João Paulo M. P. Introdução à Modelagem de Sistemas utilizando Redes de Petri, 2001. Disponível em http://www.estig.ipbeja.pt/~jpb/textos/pc/pn.pdf

Definição

“Redes de Petri é uma técnica de especificação de sistemas que possibilita uma representação matemática e possui mecanismos de análise poderosos, que permitem a verificação de propriedades e verificação da corretude do sistema especificado.”

Estrutura das Redes de Petri

LugarTransiçãoArcoMarcaArco Inibidor

1 22

21

2

Características Redes de Petri

Não-determinísticas Podem ser mapeadas em máquinas de estados Várias formas de representação:– Gráfica– Bag (conjuntos e funções matemáticas)– Matrizes– Definição por relações

Variantes de Redes de Petri

Rede Temporal, Rede Hierárquica;Rede Colorida

d

c

b

a

MarcasCores

t1

t0<a>

<c><a>

<[a,b]>

<a>

<c>

t1

t0<a>

<c><a>

<[a,b]>

<a>

<c>

Após o disparo transição t1

Propriedades das Redes de Petri

Alcançabilidade (Reachability)

Limitação (Boundedness)Liveness

Cobertura

Ferramentas

Ferramentas para verificação da corretude do modelo (checa deadlock)– ferramenta utilizada HPSim

Ferramentas para checar propriedades das redes de Petri (alcançabilidade, cobertura)– INA (

HPSim

Suporte a redes lugar-transição (sem marcas coloridas), redes com lugares com diferentes capacidades e rede temporal.

Problema do ElevadorRede de Petri Temporal e com arco inibidor

Modelagem utilizando Rede Colorida

nova_dir

dirmuda_dir

(dir,lista)

Subir|descer

dir

(dir,nova_lista)(dir,lista)

(dir,lista)(dir,nova_lista)

Lista de paradas

Lista subidasLista descidas

andar

v

(novo_mov,novo_u)(mov,u)

(mov,u)

pos

dir

i

subir|descer|parado

Funções e VariáveisOs pedidos são mantidos em quatro listas: lista_subida, lista_subida_prox (ordenadas em ordem crescente), lista_descida e lista_descida_prox (ordenadas em ordem descrecente).n - (número de andares)pos {0,...,n-1} posição do elevadorandar {0,...,n-1} (botões pressionados dentro do elevador)bot_sub,bot_des {0,...,n-1}

Funções e Variáveis

dir {subir, descer, parado}ordena_sub(par,lista) | ordena_des(par,lista) coloca o valor par na lista em ordem crescente|descrente, respectivamente

Lógica - Movimento Subida

(dir == subir) ^(andar > pos) lista_subida = ordena_sub(andar,lista_subida)(andar < pos) lista_descida_prox = ordena_des(andar,

lista_descida_prox)(bot_sub > pos) lista_subida = ordena_sub(bot_sub,lista_subida)(bot_sub < pos) lista_subida_prox =

ordena_sub(bot_sub,lista_subida_prox)(bot_des != pos) lista_descida_prox =

ordena_des(bot_des,lista_descida_prox)

Lógica - Movimento Descida

(dir == descer) ^(andar < pos) lista_descida = ordena_des(andar,lista_descida)(andar > pos) lista_subida_prox = ordena_sub(andar,

lista_subida_prox)(bot_des < pos) lista_descida =

ordena_des(bot_des,lista_descida)(bot_des > pos) lista_descida_prox =

ordena_des(bot_des,lista_descida_prox)(bot_sub != pos) lista_subida_prox =

ordena_sub(bot_sub,lista_subida_prox)

Mudando direção

quando está subindo e lista_subida fica vazia

(dir == subir) ^empty(lista_subida) ^ not_empty(lista_descida_prox) ^ (head(lista_descida_prox) >

pos){ lista_subida = cons(head(lista_descida_prox) >

pos),lista_subida) lista_descida_prox = tail(lista_descida_prox) }

Mudando direção

quando está subindo e lista_subida fica vazia

(dir == subir) ^empty(lista_subida) ^ not_empty(lista_descida_prox) ^ (head(lista_descida_prox) <= pos){ dir = descer; lista_descida = lista_descida_prox; clear(lista_descida_prox); }

Mudando direção

quando está subindo e lista_subida fica vazia

(dir == subir) ^empty(lista_subida) ^ empty(lista_descida_prox) ^ not_empty(lista_subida_prox){ dir = descer; lista_descida =

cons(head(lista_subida_prox),lista_descida); }

Mudando direçãoquando está subindo e lista_subida fica vazia

(dir == subir) ^empty(lista_subida) ^ empty(lista_descida_prox) ^empty(lista_subida_prox)

dir = parado;

Mudando direção

quando está descendo e lista_descida fica vazia

(dir == descer) ^ empty(lista_descida) ^not_empty(lista_subida_prox) ^(head(lista_subida_prox)

<= pos) { lista_descida =

cons(head(lista_subida_prox),lista_descida); lista_subida_prox = tail(lista_subida_prox);}

Mudando direção

quando está descendo e lista_descida fica vazia

(dir == descer) ^ empty(lista_descida) ^empty(lista_subida_prox) ^ not_empty(lista_descida_prox){ dir = subir; lista_subida =

cons(head(lista_descida_prox),lista_subida); lista_descida_prox = tail(lista_descida_prox);}

Mudando direção

quando está descendo e lista_descida fica vazia

(dir == descer) ^ empty(lista_descida) ^empty(lista_subida_prox) ^empty(lista_descida_prox) dir = parado;

Atualizando a lista de subida durante o movimento de subida

(dir == subir) { if (head(lista_subida) == pos) lista_subida = tail(lista_subida); pos = pos + 1;}

Atualizando a lista de descida durante o movimento de descida

(dir == descer) { if (head(lista_descida) == pos) lista_descida = tail(lista_descida); pos = pos - 1;}

Conclusões

Rede de Petri é um modelo dinâmico, não-determinístico e seu formalismo possibilita a verificação da existência de deadlocks

A rede de Petri simples possui muitas limitações, como por exemplo: não permite passagem de parâmetros e eventos temporais (Solução: uso de variantes do modelo)