Skip navigation
Use este identificador para citar ou linkar para este item: https://repositorio.ufpe.br/handle/123456789/2581
Título: Verificação de modelos para programas em um subconjunto de JCSP
Autor(es): NASCIMENTO, Carla Maria Pinheiro do
Palavras-chave: JCSP; CSP; FDR; Abstração; Regras; Refinamento
Data do documento: 2006
Editor: Universidade Federal de Pernambuco
Citação: Maria Pinheiro do Nascimento, Carla; Cabral Mota, Alexandre. Verificação de modelos para programas em um subconjunto de JCSP. 2006. Dissertação (Mestrado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2006.
Resumo: A verificação de modelos formais gerados a partir de programas concorrentes tem sido bem aceita na indústria e na academia durante a fase de testes. A busca por qualidade de software tem motivado este uso, principalmente pelo fato de que testar programas concorrentes não é uma tarefa trivial e é suscetível a erros. Os modelos são descritos através de linguagem de especificação formal para sistemas concorrentes como, por exemplo, CSP. Esta linguagem possui padrões para a descrição de interação entre sistemas concorrentes. Ela é baseada na troca de mensagens entre os componentes do sistema especificado, os processos. Cada processo é descrito através de eventos e operadores. Eventos representam as possíveis ações do usuário para com o processo ou com o ambiente (O ambiente representa o conjunto de todos os eventos visíveis aos usuários do sistema, assim como tudo o que possa interagir com os processos envolvidos no sistema { outros processos ou usuários). A biblioteca JCSP é uma biblioteca Java que possui construtores baseados em CSP. Ela provê um bom nível de abstração para a escrita de programas concorrentes sem precisarmos utilizar a estrutura de semáforos que Java oferece. Neste trabalho propomos um mapeamento entre JCSP e CSP com o intuito de estudarmos as propriedades do modelo formal gerado. Utilizamos o famoso exemplo do Jantar dos Filósofos para demonstrar a aplicação das regras, bem como suas particularidades. Propomos como estudo de caso uma modelagem para uma rede de celulares. Neste estudo apresentamos a derivação de processo regra a regra a partir de JCSP. Então analisamos o modelo gerado com o uso de FDR, um verificador de modelos para especificações concorrentes, com o objetivo de estudarmos suas propriedades clássicas (detecção de deadlocks, livelocks e não-determinismo) ou específicas da aplicação. Como principais contribuições deste trabalho podemos destacar o mapeamento de comandos Java/JCSP que possuem um maior grau de complexidade durante o mapeamento (while, atribuição, composição sequencial de comandos), visto que CSP não oferece o conceito de passagem de estado entre os comandos, como as linguagens de programação o fazem. Também podemos mencionar os construtores JCSP que não são mapeados diretamente para CSP (Alternative)
URI: https://repositorio.ufpe.br/handle/123456789/2581
Aparece na(s) coleção(ções):Dissertações de Mestrado - Ciência da Computação

Arquivos deste item:
Arquivo Descrição TamanhoFormato 
arquivo5125_1.pdf922,47 kBAdobe PDFVer/Abrir


Este arquivo é protegido por direitos autorais



Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.