trabalho-smv-2013-2

Prévia do material em texto

Trabalho sobre Verificac¸a˜o de Modelos
SIN015 – Lo´gica para Computac¸a˜o
Davi Romero de Vasconcelos
Cada equipe com no ma´ximo treˆs alunos devera´ resolver o problema sorteado em sala de aula, utilizando o
verificador de modelos SMV e a lo´gica temporal CTL. O trabalho devera´ ser entregue pelo sistema SIPPA ate´ o
dia 15 de dezembro e devera´ ser apresentado por todos os membros de cada equipe no dia 16 de dezembro,
em hora´rio a ser combinado com cada equipe.
1 Trabalho - Travessia
Considere o seguinte problema, adaptado de um livro de matema´tica para alunos do primeiro grau:
Alice, Brian, Carol e David devem atravessar uma ponte. A ponte ira´ colapsar se mais de duas pessoas estiverem
nela. Alice consegue atravessar a ponte em 1 minuto. Os outros esta˜o machucados ou feridos o que significa que
• Brian demora 2 minutos para atravessar a ponte;
• Carol demora 5 minutos para atravessar a ponte;
• David demora 10 minutos para atravessar a ponte.
Se mais de uma pessoa estiver na ponte, a ponte so´ podera´ ser atravessada na velocidade da pessoa mais
lenta. Em quanto tempo eles conseguem atravessar ponte? Considere “passaram-se X minutos”como um evento.
Especifique o modelo de Kripke associado ao comportamento de cada indiv´ıduo, levando em considerac¸a˜o os
eventos, ac¸o˜es dos outros indiv´ıduos e a configurac¸a˜o do ambiente. Obs: Na˜o e´ para especificar o modelo de
Krikpe da soluc¸a˜o do problema, e sim do problema. Especifique na lo´gica CTL o comportamento de cada
indiv´ıduo e (fo´rmula que especifica) a soluc¸a˜o do problema.
Implemente em SMV o seu modelo, utilizando-se da possibilidade de que cada indiv´ıduo seja um autoˆmato
especificado separadamente e verifique, usando a negac¸a˜o da fo´rmula que representa a soluc¸a˜o do problema, que
o mesmo tem uma soluc¸a˜o de fato.
2 Trabalho - Metroˆ
A cidade de Quixada´ esta´ projetando a construc¸a˜o de um metroˆ para solucionar o problema do transporte urbano
da cidade. Todavia, a cidade dispo˜e de poucos recursos para construir as linhas de metroˆ. Assim, a cidade tera´
apenas uma linda de metroˆ com 5 estac¸o˜es, 3 treˆns e pelo menos entre duas estac¸o˜es existe apenas um trilho
por onde os treˆns podem passar. Projete uma soluc¸a˜o de metroˆ com as restric¸o˜es acima e utilize o verificador
de modelos SMV para modelar o comportamento do controlador dos treˆns e verifique, entre outras, as seguintes
propriedades:
• Todos os treˆns circulam e passam por todas as estac¸o˜es, fazendo paradas para que os usua´rios entrem e
saiam dos trens.
• Na˜o ha´ colisa˜o entre os trens.
3 Trabalho - Edif´ıcios
Considere um edif´ıcio com 3 elevadores. Em cada andar do edif´ıcio existem dois boto˜es de chamada (para cima
e para baixo) que sinalizam todos os elevadores. Os elevadores sa˜o do tipo mais frequente, contendo boto˜es de
pedido de parada para cada andar. Existe tambe´m um sensor de peso em cada elevador que indica que o mesmo
esta´ na carga ma´xima e, portanto na˜o deve aceitar chamadas externas enquanto estiver com lotac¸a˜o ma´xima. Por
outro lado, quando um elevador ficar com carga ma´xima, ele pede mais poteˆncia do sistema ele´trico do edif´ıcio,
que foi subdimensionado para o sistema de elevadores. Assim, somente 2 elevadores podem funcionar com carga
ma´xima. O terceiro elevador, neste caso, na˜o deve se movimentar por muito tempo, somente o suficiente para
parar em seguranc¸a em algum andar. Utilize o verificador de modelos SMV para modelar o comportamento do
controlador de elevadores do pre´dio e verifique, entre outras, as seguintes propriedades:
1
• Sempre que uma pessoa chamar o elevador em um andar, via boto˜es de chamada (para cima e/ou para
baixo) o elevador vai certamente parar no respectivo andar na direc¸a˜o requisitada;
• Nunca treˆs elevadores estara˜o lotados e em movimento por mais tempo que o necessa´rio para um deles
parar em algum andar.
• Com relac¸a˜o a` parada no andar desejado, todo passageiro dentro de um elevador sempre tera´ seu pedido
atendido.
2