Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-30T13:27:45Z No. of bitstreams: 1 RafaelDeMoraisPinto_DISSERT.pdf: 1910053 bytes, checksum: 6bd105a6379f1754760bf58d58643d45 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-07-30T22:21:07Z (GMT) No. of bitstreams: 1 RafaelDeMoraisPinto_DISSERT.pdf: 1910053 bytes, checksum: 6bd105a6379f1754760bf58d58643d45 (MD5) / Made available in DSpace on 2018-07-30T22:21:07Z (GMT). No. of bitstreams: 1 RafaelDeMoraisPinto_DISSERT.pdf: 1910053 bytes, checksum: 6bd105a6379f1754760bf58d58643d45 (MD5) Previous issue date: 2016-10-14 / A necessidade por inovação e valorização de soluções criativas têm impulsionado a engenharia de requisitos a investigar técnicas de criatividade para elicitar requisitos úteis e originais. Tais técnicas baseiam-se na composição de idéias (requisitos, palavras ou problemas), geralmente vindas de fontes diversas e realizada em um processo que envolve papéis também diversos. No entanto, como identi car o núcleo comum e quais variações podem ser adaptadas ao contexto organizacional onde a técnica será usada? Esta dissertação apresenta uma Linha de Processo de Software (LPrS) para elicitação de requisitos baseada na criatividade combinacional. Esta LPrS abstrai o núcleo comum e as variações encontradas em algumas técnicas de criatividade combinacional, com o objetivo de ajudar equipes de engenharia de requisitos a de nirem a técnica combinacional de acordo com o contexto organizacional em questão. Para validar essa abordagem, discutimos como a LPrS atende às principais features dos trabalhos relacionados e como nossa LPrS generaliza as especi dades de 3 técnicas de criatividade combinacional que já foram utilizadas em estudos experimentais, produzindo resultados satisfatórios. / The need for innovation and appreciation of creative solutions has driven requirements engineering researchers to investigate creativity techniques to elicit useful and unique requirements. Such techniques are based on the combination of ideas (requirements, words or problems) that generally come from di erent sources and are carried out in a process that involves di erent roles. However, how can we identify the common core and which variations can be adapted to the organizational context where the technique will be used? This article presents a Software Process Line (SPrL) to elicit requirements based on combinational creativity. This SPrL represents commonalities and variabilities found in some combinational creativity techniques thereby it helps teams to de ne the combinational technique according their organizational context. We validate this approach by discussing how the SPrL complies with the related works' major features and how it generalizes three techniques that have already been used in experimental studies, producing satisfactory results

Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-30T13:28:52Z No. of bitstreams: 1 ValdigleisDaSilvaCosta_DISSERT.pdf: 14438862 bytes, checksum: 0296c1fddc9f8c42cbaf0336bdad7e55 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-07-30T22:29:06Z (GMT) No. of bitstreams: 1 ValdigleisDaSilvaCosta_DISSERT.pdf: 14438862 bytes, checksum: 0296c1fddc9f8c42cbaf0336bdad7e55 (MD5) / Made available in DSpace on 2018-07-30T22:29:06Z (GMT). No. of bitstreams: 1 ValdigleisDaSilvaCosta_DISSERT.pdf: 14438862 bytes, checksum: 0296c1fddc9f8c42cbaf0336bdad7e55 (MD5) Previous issue date: 2016-08-05 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / As linguagens formais definidas no final da década de 50, tem uma grande importância dentro da ciência da computação, em especial para aplicações em análise léxica e sintática dentro da construção dos compiladores e também em técnicas de inferência gramatical. A hierarquia estendida de Chomsky além de “organizar” as linguagens formais, nos possibilita traçar uma relação entre as classes de linguagens e os formalismos em termos de máquinas de estados (ou autômatos). Entre as classes de linguagens na hierarquia estão as linguagens lineares, para as linguagens desta classe existem no mínimo quatro tipos de “dispositivos”, que computam sobre elas. Entre eles estão os λ-autômatos lineares não-determinísticos propostos por Bedregal. Ao final da década de 60, Lee e Zadeh propuseram as linguagens fuzzy, numa tentativa de diminuir a distância entre as linguagens formais e as linguagens naturais. Por sua vez, Wee e Fu para capturar a noção de incerteza, durante o processo de reconhecimento de cadeias de uma linguagem, introduzem o conceito de autômatos fuzzy. Assim como na teoria clássica, podemos traçar uma relação entre as classes das linguagens fuzzy e os autômatos fuzzy. No entanto, diferente da teoria clássica, até o presente momento não existe nenhum autômato fuzzy concebido diretamente para computar sobre a classe das linguagens lineares fuzzy, isto é, que se relacione com as linguagens lineares fuzzy de forma direta. Portanto, este trabalho se propõe a realizar um estudo sobre a construção de autômatos fuzzy desenvolvidos para reconhecer as linguagens lineares fuzzy. Além disso, dado que dentro do estudo de linguagens formais, a investigação dos operadores de fecho sobre as classes de linguagens é um importante ponto, neste trabalho, iremos também investigar quais dos operadores (união, intersecção, etc) são fechados sobre as classes das linguagens lineares fuzzy. / Formal languages defined in the late 50’s play an important role in computer science, especially for applications in lexical and syntactic analysis in the construction of compilers and also in grammatical inference techniques. The extended Chomsky hierarchy in addition to “organize” formal languages, enables us to draw a relationship between the classes of languages and formalisms in terms of state machines (or automata). Among the languages classes in the hierarchy, one can find the linear languages. For such languages of this class, there are at least four types of “devices” performing computations on them. One can highlight the Nondeterministic Linear Automata, as proposed by Bedregal. In the end of the 60s, Lee and Zadeh proposed fuzzy languages in an attempt to decrease the distance between formal languages and natural languages. In turn, Wee and Fu capture the concept of uncertainty as they introduced the concept of fuzzy automata during the process of recognizing a language, similarly to the classical theory. Therefore, one can trace a relationship between the classes of fuzzy language and fuzzy automata. However, differently from the classical theory, up to now there is no designed fuzzy automata directly to compute on the class of fuzzy linear languages, i.e., relating to fuzzy linear languages directly. Therefore, this work aims to carry out a study on the construction of fuzzy automata developed to recognize the fuzzy linear languages. Furthermore, based on the study of formal languages, the investigation of the closure operators on languages classes is an important point; this work will also investigate which of the operators (union, intersection, etc.) are closed on the classes of fuzzy linear languages.

Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-30T14:57:19Z No. of bitstreams: 1 MarcosOliveiraDaCruz_DISSERT.pdf: 4332421 bytes, checksum: 11b304b7cc6ad671b40e493871db983d (MD5) / Approved for entry into archive by clediane guedes (clediane@bczm.ufrn.br) on 2018-07-31T10:52:00Z (GMT) No. of bitstreams: 1 MarcosOliveiraDaCruz_DISSERT.pdf: 4332421 bytes, checksum: 11b304b7cc6ad671b40e493871db983d (MD5) / Made available in DSpace on 2018-07-31T10:52:00Z (GMT). No. of bitstreams: 1 MarcosOliveiraDaCruz_DISSERT.pdf: 4332421 bytes, checksum: 11b304b7cc6ad671b40e493871db983d (MD5) Previous issue date: 2016-01-22 / A evolução dos processadores tem sido marcada pela crescente demanda por desempenho para atender as aplicações cada vez maiores e mais complexas. Juntamente com essa necessidade de desempenho, a heterogeneidade das aplicações exige também uma grande flexibilidade dos processadores. Os processadores convencionais são capazes de fornecer desempenho ou flexibilidade, mas sempre privilegiando um desses aspectos em detrimento do outro. Arquiteturas adaptativas aceleradoras de granularidade grossa têm sido propostas como uma solução capaz de oferecer, ao mesmo tempo, flexibilidade e desempenho. No entanto, um dos principais desafios desse tipo de arquitetura é o mapeamento de aplicações que é um problema NP-Completo. Dentre os fatores que contribuem para essa complexidade está o modelo de interconexão utilizado, que normalmente, se baseia em crossbar ou algum modelo próximo ao crossbar. Técnicas de exploração de paralelismo, como software pipelining, também são usadas para atingir melhor desempenho. Essas técnicas aumentam ainda mais a complexidade dos algoritmos de mapeamento. Este trabalho apresenta uma arquitetura adaptativa que utiliza um mecanismo de comunicação baseado em envio de pacotes para interconectar unidades funcionais. A arquitetura combinada com o modelo de interconexão é capaz de explorar paralelismo em dois níveis, a saber, ILP (incluindo técnicas de software pipeline) e TLP. O mapeamento das aplicações deve ser efetuado em tempo de compilação utilizando um algoritmo desenvolvido para a arquitetura de complexidade O(1). A arquitetura foi implementada em SystemC e a execução de diversas aplicações foi simulada, explorando tanto ILP quanto TLP. As simulações obtiveram, em média, 41% de ganho de desempenho em comparação com um processador RISC de 8 estágios de pipeline. Os resultados obtidos nas simulações confirmam que é possível explorar o paralelismo inerente das aplicações. Além disso a partir da escolha do modelo de mapeamento (como exploração de threads, ou de paralelismo no nível de instruções, laços, etc) é possível obter diferentes resultados através da adaptação da arquitetura a aplicação. / A evolução dos processadores tem sido marcada pela crescente demanda por desempenho para atender as aplicações cada vez maiores e mais complexas. Juntamente com essa necessidade de desempenho, a heterogeneidade das aplicações exige também uma grande flexibilidade dos processadores. Os processadores convencionais são capazes de fornecer desempenho ou flexibilidade, mas sempre privilegiando um desses aspectos em detrimento do outro. Arquiteturas adaptativas aceleradoras de granularidade grossa têm sido propostas como uma solução capaz de oferecer, ao mesmo tempo, flexibilidade e desempenho. No entanto, um dos principais desafios desse tipo de arquitetura é o mapeamento de aplicações que é um problema NP-Completo. Dentre os fatores que contribuem para essa complexidade está o modelo de interconexão utilizado, que normalmente, se baseia em crossbar ou algum modelo próximo ao crossbar. Técnicas de exploração de paralelismo, como software pipelining, também são usadas para atingir melhor desempenho. Essas técnicas aumentam ainda mais a complexidade dos algoritmos de mapeamento. Este trabalho apresenta uma arquitetura adaptativa que utiliza um mecanismo de comunicação baseado em envio de pacotes para interconectar unidades funcionais. A arquitetura combinada com o modelo de interconexão é capaz de explorar paralelismo em dois níveis, a saber, ILP (incluindo técnicas de software pipeline) e TLP. O mapeamento das aplicações deve ser efetuado em tempo de compilação utilizando um algoritmo desenvolvido para a arquitetura de complexidade O(1). A arquitetura foi implementada em SystemC e a execução de diversas aplicações foi simulada, explorando tanto ILP quanto TLP. As simulações obtiveram, em média, 41% de ganho de desempenho em comparação com um processador RISC de 8 estágios de pipeline. Os resultados obtidos nas simulações confirmam que é possível explorar o paralelismo inerente das aplicações. Além disso a partir da escolha do modelo de mapeamento (como exploração de threads, ou de paralelismo no nível de instruções, laços, etc) é possível obter diferentes resultados através da adaptação da arquitetura a aplicação.

Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-08-01T21:05:14Z No. of bitstreams: 1 IslameFelipeDaCostaFernandes_DISSERT.pdf: 12085812 bytes, checksum: 11b3cc3f73ed5f2051b48e441b6ee204 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-08-02T23:01:50Z (GMT) No. of bitstreams: 1 IslameFelipeDaCostaFernandes_DISSERT.pdf: 12085812 bytes, checksum: 11b3cc3f73ed5f2051b48e441b6ee204 (MD5) / Made available in DSpace on 2018-08-02T23:01:50Z (GMT). No. of bitstreams: 1 IslameFelipeDaCostaFernandes_DISSERT.pdf: 12085812 bytes, checksum: 11b3cc3f73ed5f2051b48e441b6ee204 (MD5) Previous issue date: 2018-07-06 / Conselho Nacional de Desenvolvimento Científico e Tecnológico - CNPq / O Problema da Árvore Geradora Multiobjetivo (AGMO) é uma extensão NP-Difícil da Árvore Geradora Mínima (AGM). Devido à sua habilidade em modelar inúmeros problemas reais onde objetivos conitantes devem ser otimizados simultaneamente, a AGMO tem sido intensamente estudada na literatura e muitos algoritmos exatos e heurísticos lhe foram propostos. Além disso, nos últimos anos, pesquisas têm demonstrado considerável desempenho dos algoritmos que combinam estratégias de várias meta-heurísticas. Estes algoritmos são chamados híbridos e trabalhos anteriores os aplicaram com sucesso a vários problemas de otimização. Neste trabalho, cinco novos algoritmos híbridos são propostos para duas versões da AGMO: três para a versão bi-objetivo (AG-Bi) baseada em dominância de Pareto e dois para a versão com muitos objetivos baseada no operador de média ponderada ordenada (AG-OWA). Esta pesquisa hibridizou diversas abordagens meta-heurísticas com respeito a diferentes categorias de hibridização. Experimentos computacionais avaliaram as novas abordagens com base no tempo computacional e na qualidade das soluções encontradas. Os resultados foram comparados com o estado da arte. / The Multi-objective Spanning Tree Problem (MSTP) is an NP-hard extension of the Minimum Spanning Tree (MST). Once the MTSP models several real-world problems in which conicting objectives need to be optimized simultaneously, it has been extensively studied in the literature and several exact and heuristic algorithms were proposed for it. Besides, over the last years, researchs have showed the considerable performance of algorithms that combine various metaheuristic strategies. They are called hybrid algorithms and previous works successfully applied them to several optimization problems. In this work, five new hybrid algorithms are proposed for two versions of the MSTP: three for the bi-objective version (BiST) based on Pareto dominance and two for the manyobjective version based on the ordered weighted average operator (OWA-ST). This research hybridized elements from various metaheuristics. Computational experiments investigated the potential of the new algorithms concerning computational time and solution quality. The results were compared to the state-of-the-art.

Made available in DSpace on 2016-08-31T13:33:40Z (GMT). No. of bitstreams: 1 IsaacBTS_DISSERT.pdf: 5495741 bytes, checksum: 51971b46b62abac857269a023f55e88b (MD5) Previous issue date: 2014-12-19 / Microstrip patch antennas consist of a metallic strip over a dielectric substrate and widely used because of its small size and versatility of its dimensions and possible configurations of the patch to achieve specific characteristics of resonance frequency, bandwidth, directivity and return loss. Due this versatility of its parameters, this work presents a microstrip patch antenna proposal involving the insertion of two Complementary Split Ring Resonators (CSRR), as the variation of its dimensions, and will be developed a study of CSRR s influence in antenna s parameters, designed by Transmission Line Theory, with the objective of increasing the antenna s bandwidth and filtering certain frequencies; and manufacture a device which operates in Ultra Wideband (UWB) system. The application of dielectric multilayers will be also studied with the objective of evaluate its influence in antenna s return loss. The software ANSYS HFSS® was used as an auxiliary tool to simulate the antennas parameters and the best results, as well the evaluation about the available material, were used to build the devices and measure them to validate the results previously simulated. The simulations results matched with the expected behavior of the return loss, because the filter characteristic appeared in some frequencies and the result presented a dual-band characteristic. The experimental result for the return loss agreed with the simulated pattern, despite the dislocated frequency to higher values, but just one of the measured antennas could be used in the UWB system with fractional bandwidth of 34,12% in the resonance frequency of 4,35 GHz with return loss of -36,22 dB, allowing the operation in many wireless communication systems like the IEEE standards 802.11a, 802.11n and 802.11p / As antenas de microfita tipo patch (ou plaqueta) são antenas constituídas de um recorte metálico sobre um substrato dielétrico, e são bastante utilizadas devido ao seu tamanho reduzido e versatilidade em relação as diversas configurações e dimensões que podem ser utilizadas no patch a fim de alcançar características específicas de frequência de ressonância, largura de banda, diretividade e perda de retorno. Devido a essa versatilidade em relação aos parâmetros construtivos e eletromagnéticos, este trabalho apresenta uma proposta de antena de microfita envolvendo a inclusão de dois Anéis Ressoadores Complementares (Complementary Split Ring Resonator CSRR), bem como a variação das dimensões deste, e será realizado um estudo sobre sua influência nos parâmetros da antena de microfita, projetada através da Teoria de Linha de Transmissão, objetivando o incremento da largura de banda da antena e a filtragem de determinadas faixas de frequência a fim de fabricar um dispositivo que opere no sistema Ultra Wideband (UWB). A aplicação de múltiplas camadas dielétricas também será estudada a fim de se observar sua influência na perda de retorno da antena. Os resultados foram obtidos através de simulações utilizando o software ANSYS HFSS®, que utiliza o método dos Elementos Finitos, e os melhores resultados obtidos, juntamente com a análise do material disponível, foram utilizados para a fabricação dos dispositivos e medição dos mesmos a fim de validar as simulações realizadas. Os resultados das simulações se mostraram satisfatórios, pois a característica capacitiva do CSRR permitiu o filtro de algumas faixas de frequência, fazendo com que a perda de retorno tivesse característica dual-band. O resultado experimental da perda de retorno se mostrou concordante com o padrão simulado, apesar do deslocamento de frequência, porém apenas uma das antenas construídas se adequou para aplicação no sistema UWB, com largura de banda fracionária de 34,12% para a frequência de ressonância 4,35 GHz com perda de retorno no valor de -36,22 dB, permitindo a operação desta em diversos sistemas de comunicação wireless como padrões 802.11a, 802.11n, 802.11p entre outros sistemas

Made available in DSpace on 2016-08-31T13:33:41Z (GMT). No. of bitstreams: 1 SamyaLMC_DISSERT.pdf: 2613687 bytes, checksum: 971b2c2364adeaf29f31a7eed101a113 (MD5) Previous issue date: 2014-11-20 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The use of solar panels to generate electricity is something that is becoming more common comes in both large systems, as in autonomous systems with low power consumption. So that there is maximum utilization of energy generated, the panel must always operate at maximum power point (MPP). Based on this, this paper aim to perform a comparative study of two techniques for tracking the maximum power point MPPT (Maximum Power Point Tracking): the traditional method Perturbation and Observation (P&O) and the method by Fuzzy Logic. The photovoltaic system was modeled in ATLAB/Simulink® to represent the VI characteristic curve of the PV module, which is based on data available in the catalogs of commercial photovoltaic panels. From the results of the simulation study comparing control techniques, which showed that the fuzzy controller using the best performance and efficiency in keeping the MPP than the control technique based on the P&O was done / A utilização de painéis solares fotovoltaicos na geração de energia elétrica é algo que está se tornando cada vem mais comum, tanto em sistemas de grande porte, quanto em sistemas autônomos de baixo consumo de energia. Neste sentido, objetivando o máximo aproveitamento da energia gerada, o painel deve operar sempre no ponto de máxima potência(MPP). O presente trabalho têm como objetivo realizar um estudo comparativo entre duas técnicas de rastreamento do ponto de máxima potência MPPT (Maximum Power Point Tracking): o método tradicional Perturbação e Observação (P&O) e o método através da Lógica Fuzzy. O sistema fotovoltaico foi modelado no MATLAB/Simulink® de forma a representar a curva característica V-I do módulo PV, o qual baseia-se nos dados disponíveis nos catálogos de painéis fotovoltaicos comerciais. A partir dos resultados da simulação foi feito o estudo comparativo entre as técnicas de controle, que permitiram concluir que o controlador utilizando Fuzzy apresentou melhor desempenho e eficiência em se manter no MPP do que o controle baseado na técnica P&O

A camera calibration procedure corresponds to determine the digital geometric and optical characteristics of the camera from a known initial data set. This problem can be divided into three steps: a) acquisition of initial data; b) calibration process itself; and c) optimization. This work presents the development of a calibration tool based on a generic architecture for any calibration approach. For this aim, the presented system allows the personalization of each calibration step. In the proposed tool new calibration procedures are introduced dynamically, allowing a better integration between the modules of the system. / Fundação de Amparo a Pesquisa do Estado de Alagoas / Um processo de calibração de câmera consiste no problema de determinar as características geométricas digitais e ópticas da câmera a partir de um conjunto de dados iniciais. Este problema pode ser dividido em três etapas: aquisição de dados iniciais, o processo de calibração em si e otimização. Este trabalho propõe o desenvolvimento de uma ferramenta de calibração baseada em uma arquitetura genérica para qualquer processo de calibração. Para este propósito, o sistema apresentado neste trabalho permite a personalização de cada etapa da calibração. A inclusão de novos métodos de calibração é realizada de forma dinâmica, permitindo assim maior integração e flexibilidade entre os módulos do sistema.

Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-06-15T20:18:58Z No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-06-18T19:19:46Z (GMT) No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Made available in DSpace on 2018-06-18T19:19:46Z (GMT). No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) Previous issue date: 2018-02-22 / O uso de Geradores Automáticos de Código para Métodos Formais não apenas minimiza esforços na implementação de Sistemas de Software, como também reduz a chance da existência de erros na execução destes Sistemas. Estas ferramentas, no entanto, podem ter faltas em seus códigos-fonte que causam erros na geração dos Sistemas de Software, e então a verificação de tais ferramentas é encorajada. Esta tese de Doutorado visa criar e desenvolver uma estratégia para verificar JCircus, um Gerador Automático de Código de um amplo sub-conjunto de Circus para Java. O interesse em Circus vem do fato de que ele permite a especificação dos aspectos concorrentes e de estado de um Sistema de maneira direta. A estratégia de verificação consiste nos seguintes passos: (1) extensão da Semântica Operacional de Woodcock e prova de que ela é sólida com respeito à Semântica Denotacional existente de Circus na Teoria Unificada de Programação (UTP), que é um framework que permite prova e unificação entre diferentes teorias; (2) desenvolvimento e implementação de uma estratégia que verifica o refinamento do código gerado por JCircus, através de uma toolchain que engloba um Gerador de Sistema de Transições Rotuladas com Predicado (LPTS) para Circus e um Gerador de Modelos que aceita como entrada (I) o LPTS e (II) o código gerado por JCircus, e gera um modelo em Java Pathfinder que verifica o refinamento do código gerado por JCircus. Através da aplicação do passo (2) combinada com técnicas baseadas em cobertura no código fonte de JCircus, nós visamos aumentar a confiabilidade do código gerado de Circus para Java. / The use of Automatic Code Generators for Formal Methods not only minimizes efforts on the implementation of Software Systems, but also reduces the chance of existing errors on the execution of such Systems. These tools, however, can themselves have faults on their source codes that may cause errors on the generation of Software Systems, and thus verification of such tools is encouraged. This PhD thesis aims at creating and developing a strategy to verify the code generation from the Circus formal method to Java Code. The interest in Circus comes from the fact that it allows the specification of concurrent and state-rich aspects of a System in a straightforward manner. The code generation envisaged to be verified is performed by JCircus, a tool that translates a large subset of Circus to Java code that implements the JCSP API. The strategy of verification consists on the following steps: (1) extension of Woodcock’s Operational Semantics to Circus processes and proof that it is sound with respect to the Denotational Semantics of Circus in the Unifying Theories of Programming (UTP), that is a framework that allows proof and unification of different theories; (2) development and implementation of a strategy that refinement-checks the code generated by JCircus, through a toolchain that encompasses (2.1) a Labelled Predicate Transition System (LPTS) Generator for Circus and (2.2) a Model Generator that inputs (I) a LPTS and (II) the code generated by JCircus, and generates a model (that uses the Java Pathfinder code model-checker) that refinement-checks the code generated by JCircus. Combined with coverage-based techniques on the source code of JCircus, we envisage improving the reliability of the Code Generation from Circus to Java.

Uma metapopulação pode ser definida como uma população regional de populações locais geograficamente distintas, interconectadas por migração. Dentro deste contexto, modelos de dinâmica metapopulacional espacialmente implícitos descrevem a taxa de variação da proporção de manchas ocupadas por uma ou mais espécies por meio de um balanço entre os processos de colonização de manchas vazias e extinção de manchas ocupadas. O modelo metapopulacional de Levins prevê que mesmo na presença de habitat adequado, uma espécie pode se extinguir regionalmente, de forma determinística, se a intensidade de extinção for maior do que a intensidade de colonização. Além disso, este modelo sugere a existência de uma quantidade limiar de habitat remanescente, abaixo do qual a extinção regional determinística da espécie ocorre. Características importantes da dinâmica espacial, tais quais, efeito Allee, efeito resgate, colonização externa, qualidade da matriz, efeito anti-resgate e heterogeneidade de manchas podem ser incluídas em variantes do modelo de Levins. Uma outra extensão natural desses modelos é o agrupamento das manchas com relação ao seu estado de ocupação em modelos de metapopulações de espécies interativas, dando origem aos modelos de metacomunidades. Estudos de dinâmica de metacomunidades permitem a análise das relações entre a diversidade de espécies e a heterogeneidade ambiental no nível da paisagem, bem como as implicações de interações diretas e indiretas para a estrutura de comunidades.

O uso de sistemas quâticos como parte de sistemas de comunicação tem sido fonte de interessantes problemas muitos ainda sem solução. No presente trabalho, apresentamos os conceitos básicos em teoria da informação e mecânica quântica necessários ao entendimento do problema do cálculo da informação acessível, cuja solução maximiza a informação mútua de Shannon para um canal definido por um ensemble de estados quâticos dados a priori. Propomos o uso do método de otimização global Branch and Bound aliado à aritmética intervalar para a estimação de limites mais precisos que os teóricos disponíveis para a informação acessível. Experimentos numéricos e resultados relacionados são apresentados. / The use of quantum systems as part of the communication systems has been source of interesting problems many without solution. In the present work, we show the basic concepts of information theory and quantum mechanics necessary to understand the accessible information problem, whose solution maximizes the Shannon mutual information for a channel defined by an ensemble of quantum states given a priori. In order to estimate more precise bounds for accessible information, we propose the use of Branch and Bound method with interval arithmetic. Numerical experiments and related results are exhibited.