Return to search

Verificação de modelos para programas em um subconjunto de JCSP

Made available in DSpace on 2014-06-12T15:59:26Z (GMT). No. of bitstreams: 2
arquivo5125_1.pdf: 944608 bytes, checksum: b3965877c4e7cb64788c8157f6ca6838 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2006 / 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)

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/2581
Date January 2006
CreatorsNASCIMENTO, Carla Maria Pinheiro do
ContributorsMOTA, Alexandre Cabral
PublisherUniversidade Federal de Pernambuco
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Sourcereponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0023 seconds