Especificação de Sistemas
Distribuídos
Modelo CSPm - Estacionamento
Equipe:
Rafael Araújo ([email protected])
Ingridd Brito ([email protected])
Sistema
• Sistema de estacionamento de um local genérico;
• Possui possibilidade de pagamento tanto em um Caixa quanto na Cancela
de Saída (caso o pagamento seja necessário);
• O pagamento pode ser realizado utilizando cartão de crédito ou dinheiro se
realizado no Caixa;
• Se realizado na Cancela de Saída, o único meio aceito é via cartão de
crédito.
Sistema
• Os veículos poderão entrar por uma das Cancelas de Entrada disponíveis;
• Os mesmos poderão realizar o pagamento no caixa, dadas as devidas
sincronizações;
• Ou podem realizar o mesmo na Cancela de Saída;
• O Servidor é responsável por armazenar e gerenciar a sequência de tuplas
(placa, hora) dos carros que entram no estacionamento através da Cancela
de Entrada.
Componentes
• O sistema é composto por:
• Datatypes, conjuntos e sequências;
• Funções.
• Canais e eventos;
• Processos;
Datatypes, Conjuntos e Sequências
• Datatypes:
• datatype
PLACAS = KGC3920 | KHJ2103 | KLA9123 |
KFL1984
• Representam as placas dos veículos;
Datatypes, Conjuntos e Sequências
• Datatypes:
• datatype
MENSAGEM= RetireTicket | PlacaExistente|
BemVindo| TempoEsgotado| Obrigado
• Representam as mensagens que são exibidas para o usuário/veículo durante
algumas das operações;
Datatypes, Conjuntos e Sequências
•
•
•
•
•
Alguns dos conjuntos presentes no sistema:
RANGE = {1..3} //Capacidade de determinados processos.
HORA = {1200, 1300, 1400, 1500} -- Simulam um horário de
entrada de um veículo.
VEICULOS = {1..2} // Quantidade de veículos.
Representam as mensagens que são exibidas para o usuário/veículo durante algumas das
operações;
Datatypes, Conjuntos e Sequências
• Sequência utilizada no Sistema:
• TICKETS
= <>
• Esta sequência armazena pares de placas e horas (i.e. (KGC3920, 1200)) de
modo a representar os horários os quais as placas (veículos) entraram no
estabelecimento.
Funções
•
•
•
•
Funções utilizadas no sistema (assinaturas):
placaJaCadastrada(p, <>)
placaJaCadastrada(p, <(placa, hora)> ^ ticketsRestantes)
Utilizada para determinar se uma placa já existe na sequência para que não haja
veículos com a mesma placa em horários diferentes.
Funções
• Funções utilizadas no sistema (assinaturas):
• GetHora(p,
t) = { h | h <- HORA, elem((p, h), t) }
• Utilizada para retornar um horário de entrada (h) relacionado a uma
determinada placa (representada por p).
Funções
•
•
•
•
Funções utilizadas no sistema (assinaturas):
RemovePlaca(placa, <>) = <>
RemovePlaca(p, <(placa, hora)> ^ placasRestantes)
Utilizada para remover a placa de uma sequência, onde a entrada é dada por uma própria
sequência que é dividida em head e tail através da concatenação de elementos e é analisada
separadamente até que a placa desejada seja encontrada, então, a concatenação dos elementos
previamente analisados e os restantes serão retornados como uma única sequência.
Canais e Eventos
• Alguns dos Canais de Dados e Eventos presentes no sistema:
• channel
levantaCancela, baixaCancela
• Representam ações de um processo que não recebem dados, normalmente
utilizadas como alfabeto de sincronização ou operações únicas;
Canais e Eventos
•
Alguns dos Canais de Dados e Eventos presentes no sistema:
•
channel enviaDados: RANGE.PLACAS.HORA
•
Representam ações de um processo que recebem dados, onde há a comunicação
(output) de um processo X para a entrada (input) de um processo Y. Estas
representam operações que operam sobre dados ou que irão gerar eventos
baseados em valores transientes (calculados) sobre tais dados;
Processos
•
•
•
Exemplo de Processo encontrado no sistema:
CancelaEntrada(n) = recebeDados!n?p -> leHora!n?hora ->
enviaDados!n!p!hora -> entregaTicket.n -> abrirCancela.n
-> display!BemVindo-> fecharCancela.n ->
CancelaEntrada(n)
Representam um conjunto de ações (eventos) com trasmissão de dados ou não,
estes denotam o comportamento do processo de maneira contínua;
Processos
•
•
•
Exemplo de Processo encontrado no sistema:
Servidor(T) = (enviaDados?n?placa?hora -> if (not
placaJaCadastrada(placa, T)) then Servidor(T ^ <(placa,
hora)>) else display!PlacaExistente -> Servidor(T))
Neste caso, faz-se o uso da sequência presente no sistema, estruturas de controle
if-then-else e avaliação de expressões provenientes de funções.
Avaliações
•
•
•
•
•
Para determinar algumas propriedades do sistema são utilizadas algumas asserções, tais como:
assert CancelaEntrada(1) :[deterministic]
assert CancelaEntrada(1) :[deadlock free]
assert CancelaEntrada(1) :[livelock free]
Estas representam, respectivamente, a presença de determinismo em um processo (ou
composições, escolhas, etc. entre eles), a presença de deadlock e livelock, dada a análise unitária
ou em conjunto com outros processos.
Avaliações
•
Exemplo de asserções relativas a interação entre processos:
•
CancelaEntradaANDVeiculo = CancelaEntrada(1) [|{|recebeDados|}|]
Veiculo(1)
•
•
•
assert CancelaEntradaANDVeiculo :[deterministic]
•
assert CancelaEntradaANDVeiculo :[deadlock free]
assert CancelaEntradaANDVeiculo :[livelock free]
Mesmos conceitos presentes na análise de um único processo, a diferença é a avaliação como um todo para
quaisquer processos envolvidos e suas operações, havendo sincronização ou não.
Refinamento
• Para availiar se um processo "melhora" o outro em determinado modelo
(Traces, Falhas, Falhas-Divergências) foram utilizadas as seguintes
asserções:
assert TotalVeiculos_UNREF [T= TotalVeiculos_REF
assert TotalVeiculos_UNREF [F= TotalVeiculos_REF
assert TotalVeiculos_UNREF [FD= TotalVeiculos_REF
Refinamento
•
Para esta avaliação, foram utilizados os seguintes processos:
•
TotalVeiculos_UNREF = |~| x: VEICULOS @ Veiculo(x) -Processo com não-determinismo proposital, proveniente da
escolha interna
•
TotalVeiculos_REF = [] x: VEICULOS @ Veiculo(x) -Processo que refinará o anterior, utilizando escolha
externa
Melhorias no Modelo
• Interação entre Processos da Cancela de Saída e Veículo;
• Utilização do servidor ao sincronizar dados com o Caixa, ao invés de utilizar
uma função como filtro de valores.
Considerações Finais
• Todos os processos foram avaliados nas 3 proposições de asserção;
• Deadlocks esperados estão marcados no modelo (.csp);
• Operações de dados foram realizadas utiizando índices para indicar qual o
evento e qual o processo que originou este evento, durante a sincronização /
paralelismo.