Biblioteca em CSP
Disciplina: Especificação de Sistemas Distribuídos - ESD
Professor: Alexandre Mota
Semestre: 2014.1
Alunos: Alex Candido - aacs
Jacinto Filipe - jfsr
Agenda
●
●
●
●
●
●
●
●
●
●
●
Introdução & Objetivo
Ilustração Textual do Projeto
Ilustração Visual do Projeto
Principais Constantes
Principais Tipos
Principais Canais
Principais Processos
Composição do Sistema
Não Determinismo (intencional)
Refinamento do Não Determinismo
Dificuldades Enfrentadas
Introdução & Objetivo
● O objetivo deste trabalho é tentar modelar um sistema do mundo real que
torne possível a aplicação prática de alguns dos conceitos vistos em sala
de aula.
● O sistema escolhido foi o de uma Biblioteca, tendo em vista que esse
sistema é constituído de entidades comunicantes que permitem aplicar os
conceitos de concorrência e paralelismo.
Ilustração Textual (p.1)
●
O Usuário ao chegar na biblioteca irá procurar e pegar o livro desejado, tendo assim uma lista
de livros escolhidos, que por sua vez não pode ser maior que o tamanho máximo da lista de
livros.
●
Após ter escolhido os livros, o Usuário pode decidir em Realizar o Empréstimo se dirigindo
para o balcão, onde irá interagir com o Bibliotecário, e assim Finalizar o Empréstimo por
meio de uma Autenticação, que é composta pela Validação do Usuário através da verificação
do seu CPF e Senha.
●
O Bibliotecário inicia a sessão e passa a aguardar pelo usuário até que o mesmo decida
Realizar um Empréstimo e ele passa a atender o usuário, a ler as informações dos livros
contidos no balcão usando o scanner até Finalizar o Empréstimo e então ele passar a
Esperar pela Autenticação do Usuário, gerando com isso um Comprovante em caso de
sucesso.
Ilustração Textual (p.2)
●
O Computador, por sua vez tem interação direta com o Bibliotecário, uma vez que após ter o
Acervo Carregado no sistema, o Computador está sem Bibliotecário. Após ocorrer uma
interação entre o Bibliotecário e um Computador iniciando uma sessão, o Computador
torna-se disponível podendo Realizar um Empréstimo ou ter sua sessão encerrada, ficando
o Computador sem Bibliotecário.
●
Caso o Bibliotecário seja acionado Realizar um Empréstimo, o Computador entra em
Utilização e irá continuar nesse estado enquanto o Bibliotecário lê as informações dos livros
usando o scanner até Finalizar o Empréstimo e assim o Computador passa a esperar pela
Autenticação do Usuário.
●
Como mencionado anteriormente, tal validação acontece através da verificação do seu CPF e
Senha. Em caso positivo, uma Resposta positiva é exibida e um comprovante será gerado,
tornando o Computador disponível novamente, caso contrário, uma Resposta negativa é
exibida e o Computador permanece esperando pela Autenticação.
Ilustração Textual (p.3)
● O Servidor da Biblioteca é a entidade responsável por Enviar o Acervo
para a Biblioteca, isso só acontece após o mesmo estar ligado, ficando
Disponível.
● Uma vez que o Servidor da Biblioteca está disponível, o mesmo pode
ser Desligado, pode Carregar o Acervo e por fim, Registro de
Empréstimos do Computador, que nada mais é do que o somatório dos
registros de empréstimos da Biblioteca
mais a quantidade de
empréstimo contida no comprovante.
Ilustração Visual 1 (Usuário)
Ilustração Visual 2 (Bibliotecário)
Ilustração Visual 3 (Computador)
Ilustração Visual 4 (Servidor bibl.)
Principais Constantes
●
●
●
●
●
●
●
●
tamanhoMaximoDoAcervo = 2
tamanhoMaximoDoComprovante = 2
tamanhoMaximoDoRegistoDeEmprestimos = 2
tamanhoMaximoDaListaDeLivros = 2
qtdBibliotecarios = 2
qtdComputadores = 2
qtdUsuarios = 2
qtdBibliotecas = 1
Principais Tipos
●
●
●
●
●
●
●
●
●
●
datatype Resposta = usuarioInexistente | usuarioEncontrado
Livro = {1..1}
Bibliotecario = {1..qtdBibliotecarios}
Computador = {1..qtdComputadores}
Usuario = {1..qtdUsuarios}
Biblioteca = {1..qtdBibliotecas}
Acervo = union({<livro>| livro <- Livro},{<>})
Comprovante = union({<livro>| livro <- Livro},{<>})
Cpf = { getCpf(usuario) | usuario <- Usuario }
Senha = { getSenha(cpf) | cpf <- Cpf }
Principais Canais
●
●
●
●
●
●
●
●
●
●
●
●
●
channel RealizarEmprestimo, FinalizarEmprestimo: Bibliotecario
channel PegarLivro : Livro
channel Balcao : Bibliotecario.Livro
channel DigitarCpf, VerificacaoCpf : Bibliotecario.Cpf
channel DigitaSenha, VerificacaoSenha : Bibliotecario.Cpf.Senha
channel ValidarUsuario : Bibliotecario.Resposta
channel Scanner : Bibliotecario.Livro
channel Impressora : Bibliotecario.Comprovante
channel IniciarSessao, EncerrarSessao : Bibliotecario
channel LigarServidorDaBiblioteca, DesligarServidorDaBiblioteca : Biblioteca
channel CarregarRegistrosDeEmprestimoDoComputador : Comprovante
channel CarregarAcervo : Biblioteca.Acervo
channel EnviarAcervoParaBiblioteca : Acervo
Principais Processos
●
●
●
●
●
●
●
●
●
●
●
●
●
●
●
USUARIO
USUARIO_NO_BALCAO
USUARIO_SE_AUTENTICANDO
BIBLIOTECARIO
BIBLIOTECARIO_AGUARDANDO_USUARIO
BIBLIOTECARIO_EM_ATENDIMENTO
BIBLIOTECARIO_ESPERANDO_AUTENTICACAO
COMPUTADOR
COMPUTADOR_SEM_BIBLIOTECARIO
COMPUTADOR_DISPONIVEL
COMPUTADOR_EM_UTILIZACAO
COMPUTADOR_ESPERANDO_AUTENTICACAO
SERVIDOR_DA_BIBLIOTECA
SERVIDOR_DA_BIBLIOTECA_DISPONIVEL
BD_USUARIOS_BIBLIOTECA
Composição do Sistema
Canais_Bibliotecario_Computador = {|IniciarSessao, EncerrarSessao,Scanner, RealizarEmprestimo,
FinalizarEmprestimo, VerificacaoCpf, VerificacaoSenha, ValidarUsuario, Impressora|}
Canais_Biblioteca_Servidor = {|CarregarAcervo|}
Canais_Sistema_Usuario = {|RealizarEmprestimo,FinalizarEmprestimo,Balcao,DigitarCpf,DigitaSenha,ValidarUsuario|}
Canais_Computador_BD = {|VerificacaoCpf,VerificacaoSenha,ValidarUsuario|}
BIBLIOTECARIOS = ||| b:{1..qtdBibliotecarios}@ (BIBLIOTECARIO(b))
CONJUNTO_COMPUTADOR_BD(biblioteca) =
(COMPUTADOR(biblioteca) [|Canais_Computador_BD|] BD_USUARIOS_BIBLIOTECA)
CONJUNTO_BIBLIOTECARIO_COMPUTADOR(biblioteca) =
(BIBLIOTECARIOS [|Canais_Bibliotecario_Computador|] CONJUNTO_COMPUTADOR_BD(biblioteca))
BIBLIOTECA(biblioteca) =
(CONJUNTO_BIBLIOTECARIO_COMPUTADOR(biblioteca)[|Canais_Biblioteca_Servidor|]
SERVIDOR_DA_BIBLIOTECA(biblioteca))
BIBLIOTECAS = ||| b:{1..qtdBibliotecas}@ (BIBLIOTECA(b))
USUARIOS = ||| u:{1..qtdUsuarios}@ (USUARIO(u,<1>))
SISTEMA = BIBLIOTECAS [|Canais_Sistema_Usuario|] USUARIOS
Não Determinismo (intencional)
●
A utilização intencional do operador de Escolha Interna possibilita a simulação se um usuário
existe ou não no banco de dados dos usuários da biblioteca.
BD_USUARIOS_BIBLIOTECA =
VerificacaoCpf?bibliotecario?cpf ->
VerificacaoSenha.bibliotecario.cpf.getSenha(cpf) ->
(
ValidarUsuario.bibliotecario!usuarioEncontrado ->
BD_USUARIOS_BIBLIOTECA
|~|
ValidarUsuario.bibliotecario!usuarioInexistente ->
BD_USUARIOS_BIBLIOTECA
)
Refinamento do Processo
●
A utilização do operador de Escolha Externa, possibilita a remoção do comportamento Não
Determínistico do processo.
BD_USUARIOS_BIBLIOTECA =
VerificacaoCpf?bibliotecario?cpf ->
VerificacaoSenha.bibliotecario.cpf.getSenha(cpf) ->
(
ValidarUsuario.bibliotecario!usuarioEncontrado ->
BD_USUARIOS_BIBLIOTECA
[]
ValidarUsuario.bibliotecario!usuarioInexistente ->
BD_USUARIOS_BIBLIOTECA
)
Dificuldades Enfrentadas
● Encontrar um projeto/tema o qual fossemos capazes de elaborar dentro
do prazo e grau de complexidade compatível com o nível de
conhecimento da dupla.
● Realizar o mapeamento das entidades do mundo real para o virtual.
● Falta de experiência com modelagens em geral, e principalmente com a
linguagem CSP.
● Entender e conseguir separar as estruturas/entidades.
● Pensar de maneira concorrente e paralela, além de compreender como as
estruturas se comunicam.
● Compreender e reconhecer na prática os principais conceitos abordados
durante a disciplina, como: Deadlock, Não Determinismo e Livelock.