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)

Made available in DSpace on 2014-06-12T16:01:28Z (GMT). No. of bitstreams: 2 arquivo9411_1.pdf: 1518901 bytes, checksum: d645deca05140af7b59c0d3726ee9757 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Com o advento de processadores multicore, a programação concorrente ganhou importância e tem se tornado um dos grandes desafios da área de engenharia de software. O paradigma de programação concorrente, implementado por linguagens de programação como Java, C, e C++, oferece um nível de expressividade muito baixo, dificultando a sua utilização. Aliado a isso, o uso de bibliotecas que implementam abstração de concorrência, requer um esforço de aprendizado adicional, como também produz programas cuja lógica da regra de negócio está entrelaçada com chamadas para a biblioteca que implementa concorrência de forma mais abstrata. O presente trabalho propõe separar o código concorrente daquele usado no desenvolvimento de código sequencial Java. Todo comportamento concorrente é extraído do código e torna-se anotações de classe. Tais anotações seguem a sintaxe da linguagem CSP, uma linguagem formal que foi criada para descrever sistemas concorrentes e distribuídos. Para prover esta separação, este trabalho sugere um compilador, chamado AJCSP, o qual reconhece as anotações nas classes Java, gerando código concorrente utilizando a biblioteca JCSP. A programação orientada a aspectos foi explorada para instrumentar o programa sequencial Java com construções concorrentes contidas no código gerado. Para avaliar o framework proposto, foram utilizadas métricas de separação de preocupações (SoC), acoplamento, bem como tamanho em cinco sistemas distintos implementados nas diferentes abordagens de concorrência (java thread, JCSP e AJCSP). A avaliação obtida demonstrou que, quando utilizado AJCSP, a quantidade de linhas de código do sistema diminui, assim como a dependência com a biblioteca de concorrência

Made available in DSpace on 2014-12-17T15:47:56Z (GMT). No. of bitstreams: 1 SAMUEL LINCOLNdissertacao_final.pdf: 2269762 bytes, checksum: f3ae8e1d8966bfbf455c79b080c96cc2 (MD5) Previous issue date: 2011-08-29 / This dissertation aims at extending the JCircus tool, a translator of formal specifications into code that receives a Circus specification as input, and translates the specification into Java code. Circus is a formal language whose syntax is based on Z s and CSP s syntax. JCircus generated code uses JCSP, which is a Java API that implements CSP primitives. As JCSP does not implement all CSP s primitives, the translation strategy from Circus to Java is not trivial. Some CSP primitives, like parallelism, external choice, communication and multi-synchronization are partially implemented. As an aditional scope, this dissertation will also develop a tool for testing JCSP programs, called JCSPUnit, which will also be included in JCircus new version. The extended version of JCircus will be called JCircus 2.0. / Esta disserta??o tem como objetivo estender a ferramenta JCircus, um tradutor de especifica??es formais para c?digo que recebe uma especifica??o em Circus como entrada, e traduz a especifica??o para c?digo Java. Circus ? uma linguagem formal cuja sintaxe ? baseada nas sintaxes das linguagens Z e CSP. O c?digo gerado por JCircus faz uso de JCSP, que ? uma API de Java que implementa primitivas de CSP. O fato de JCSP n?o implementar CSP completamente faz com que a estrat?gia de tradu??o de Circus para Java seja n?o-trivial. Algumas primitivas de CSP, como paralelismo, escolhas externa e interna, comunica??o, e multi-sincroniza??o s?o implementadas em JCSP de forma parcial. Nesta disserta??o, estendemos a tradu??o destas primitivas. Al?m disso, esta disserta??o tamb?m desenvolver? uma ferramenta para fazer testes em processos JCSP, chamada JCSPUnit.