Linha de Fabrico


Pretende-se modelar um sistema de transporte de uma linha de fabrico. Esta é constituida por uma série de mesas, existindo um braço robotizado entre cada par de mesas. O braço 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

Algumas das propriedades que o 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.

Notas

Este problema deve ser modelado usando redes de petri e a ferramenta de verificação de modelos 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 ensinadas. As propriedades enumeradas devem ser verificadas pelo modelo a apresentar. Sempre que possível devem ser demonstradas usando técnicas estruturais (como invariantes de lugar), mas também usando verificação de modelos. Para tal terão que ser traduzidas em fórmulas CTL equivalentes. Se desejarem podem enriquecer a especificação adicionando novas características ao modelo ou novas propriedades para verificar. Naturalmente, tal será valorizado na nota final.