...collaborate on

Elementos Lógicos da Programação III

Projecto Prático

Pretende-se que modele e analise os dois problemas seguintes usando redes de petri e a ferramenta de model checking SMV. Na modelação deve começar por usar uma rede colorida e depois fazer a seu expansão para uma rede normal. Nesta operação pode começar por usar capacidades e arcos inibidores, que depois deverão ser eliminados usando as regras de transformação já ensinadas. Para cada problema são enumeradas algumas propriedades que devem ser verificadas pela solução apresentada. Sempre que possível devem ser demonstradas usando técnicas estruturais (como invariantes de lugar), mas também usando model checking. Para tal terão que ser traduzidas em fórmulas CTL equivalentes. Sempre que desejarem, podem enriquecer a especificação adicionando novas características ao modelo ou novas propriedades para verificar. Naturalmente, tal será valorizado na nota final.

O projecto é facultativo. Deverá ser realizado em grupos com o máximo de dois alunos. A apresentação será em data a combinar, devendo na mesma ser entregue um pequeno relatório com a descrição das tarefas realizadas.

ATENÇÃO: esta página será alterada consoante a necessidade de clarificar o enunciado.

Sistema de Transporte

Pretende-se modelar um sistema de transporte de uma linha de produção. Esta é constítuida por uma série de mesas, existindo um braço robotizado entre cada par de mesas. O braço robotizado pode estar em três posições diferentes (A, B e C), podendo mover-se para a esquerda ou para a direita. Também possui uma garra que lhe permtite apanhar uma peça numa mesa e transportá-la para a seguinte. Considere também que existe um produtor que coloca as peças na primeira mesa e um consumidor que as retira da última.

Trans.jpg

Algumas das propriedades que a sistema modelado deve verificar são:

  • Cada mesa pode conter no máximo uma peça.
  • Não deve possível colocar uma peça na mesa i se o robot i está na posição A.
  • Nomeadamente, nunca deve ser possível o robot i estar na posição C e o robot i+1 na posição A.
  • Os motores de deslocamento para a esquerda e para a direita não podem estar activos simultaneamente.
  • Qualquer peça que seja colocada na primeira mesa deve eventualmente chegar à última.
  • Não existem deadlocks.

Exclusão Mútua Distribuída

Pretende-se implementar um algoritmo de exclusão mútua distribuído, ou seja sem nenhum controlador centralizado. O mesmo será baseado no conceito token ring. As diversas unidades funcionais estão ligadas através de um anel de comunicação onde circula uma marca. Sempre que uma unidade pretende entrar na zona crítica deverá retirar esta marca do anel, devendo a mesma ser propagada para a unidade seguinte quando não for necessária. A seguinte imagem apresenta um esquema da rede de petri que modela este problema, para o caso em que temos três unidades funcionais, estando uma delas detalhada.

Ring.jpg

Cada unidade é constituída por dois módulos:

  • O primeiro, cuja rede se encontra detalhada, representa o componente que pretende usar o recurso crítico. Tem três estados possíveis: Idle, quando está a realizar tarefas que não envolvem o recurso crítico; Waiting, quando está à espera de usar o recurso crítico; e Critical, quando está na zona de exclusão mútua.
  • O segundo é o controlador que irá implementar o protocolo, e cuja especificação é o objectivo deste projecto.

A comunicação entre os dois componentes é feita assincronamente usando os lugares Req (request), Prm (permission), e Rdy (ready). O primeiro é usado para sinalizar a vontade de usar o recurso crítico. O segundo é usado pelo controlador para dar autorização ao outro componente para entrar na zona crítica, e o último serve para este indicar que já terminou a utilização do recurso crítico. O controlador também tem acesso ao anel onde circula a marca. Sempre que deseje, pode retirar a mesma da sua porta de entrada (Tok) ou transferi-la para a unidade funcional que lhe sucede no anel.

Algumas das propriedades que a solução deve verificar são:

  • Não existem duas unidades simultaneamente na zona crítica.
  • Não existem deadlocks.
  • Nunca existe mais do que uma marca a circular no anel.
  • Qualquer unidade que pretenda utilizar o recurso crítico poderá eventualmente fazê-lo.
  • Uma unidade não poderá utilizar o recurso crítico duas vezes seguidas se outra unidade também o pretender utilizar.
  • A marca não deve circular desnecessariamente pelo anel. Só o deverá fazer se alguma unidade requisitar o acesso à zona crítica.

Para poder satisfazer esta última propriedade poderá ser necessário adicionar um segundo anel de comunicação (com sentido inverso) onde circulam pedidos para libertar a marca.

r3 - 05 Apr 2005 - 07:48:18 - AlcinoCunha
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
Syndicate this site RSSATOM