Skip navigation
Please use this identifier to cite or link to this item: https://repositorio.ufpe.br/handle/123456789/2581
Title: Verificação de modelos para programas em um subconjunto de JCSP
Authors: NASCIMENTO, Carla Maria Pinheiro do
Keywords: JCSP;CSP;FDR;Abstração;Regras;Refinamento
Issue Date: 2006
Publisher: Universidade Federal de Pernambuco
Citation: 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.
Abstract: 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
Appears in Collections:Dissertações de Mestrado - Ciência da Computação

Files in This Item:
File Description SizeFormat 
arquivo5125_1.pdf922.47 kBAdobe PDFView/Open


This item is protected by original copyright



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.