Search

Submitted by Rafael Menezes (rafael.sa@icomp.ufam.edu.br) on 2021-09-02T19:12:38Z No. of bitstreams: 3 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) dissertacao-final.pdf: 2519519 bytes, checksum: 62c5a24015685b1b75954c32c0135995 (MD5) CartaEncaminhamentoTCC-TESE-DISSERTA????O.pdf: 112019 bytes, checksum: 1966306a36cb2747e5a887f896a370a2 (MD5) Approved for entry into archive by PPGI Inform??tica (secretariappgi@icomp.ufam.edu.br) on 2021-09-06T19:16:07Z (GMT) No. of bitstreams: 3 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) dissertacao-final.pdf: 2519519 bytes, checksum: 62c5a24015685b1b75954c32c0135995 (MD5) CartaEncaminhamentoTCC-TESE-DISSERTA????O.pdf: 112019 bytes, checksum: 1966306a36cb2747e5a887f896a370a2 (MD5) Rejected by Divis??o de Documenta????o/BC Biblioteca Central (ddbc@ufam.edu.br), reason: O dep??sito precisa de ajuste: 1. Na disserta????o, retirar as folhas em branco que se intercalam entre as demais. 2. Na ficha catalogr??fica, as palavras-chave devem iniciar em letra mai??scula, portanto: "1. Bounded Model Checking. 2. Caching. 3. Software. 4. Verification. 5. Testcase generation." 3. A disserta????o possui 54 folhas, n??o 71 como informada na ficha. O campo deve ser corrigido. on 2021-09-06T20:51:34Z (GMT) Submitted by Rafael Menezes (rafael.sa@icomp.ufam.edu.br) on 2021-09-15T16:33:21Z No. of bitstreams: 3 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) CartaEncaminhamentoTCC-TESE-DISSERTA????O.pdf: 112019 bytes, checksum: 1966306a36cb2747e5a887f896a370a2 (MD5) dissertacao-final.pdf: 2500824 bytes, checksum: c7dedc42fc1d8850003605631825473a (MD5) Approved for entry into archive by PPGI Inform??tica (secretariappgi@icomp.ufam.edu.br) on 2021-09-16T13:41:23Z (GMT) No. of bitstreams: 3 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) CartaEncaminhamentoTCC-TESE-DISSERTA????O.pdf: 112019 bytes, checksum: 1966306a36cb2747e5a887f896a370a2 (MD5) dissertacao-final.pdf: 2500824 bytes, checksum: c7dedc42fc1d8850003605631825473a (MD5) Approved for entry into archive by Divis??o de Documenta????o/BC Biblioteca Central (ddbc@ufam.edu.br) on 2021-09-16T15:03:38Z (GMT) No. of bitstreams: 3 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) CartaEncaminhamentoTCC-TESE-DISSERTA????O.pdf: 112019 bytes, checksum: 1966306a36cb2747e5a887f896a370a2 (MD5) dissertacao-final.pdf: 2500824 bytes, checksum: c7dedc42fc1d8850003605631825473a (MD5) Made available in DSpace on 2021-09-16T15:03:38Z (GMT). No. of bitstreams: 3 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) CartaEncaminhamentoTCC-TESE-DISSERTA????O.pdf: 112019 bytes, checksum: 1966306a36cb2747e5a887f896a370a2 (MD5) dissertacao-final.pdf: 2500824 bytes, checksum: c7dedc42fc1d8850003605631825473a (MD5) Previous issue date: 2021-06-08 CNPq - Conselho Nacional de Desenvolvimento Cient??fico e Tecnol??gico Testcase generation consists in generating inputs for an algorithm that are able to explore all paths of a program, maximizing its coverage. Usually, fuzzing techniques are used because of its great performace and low cost. However, formal techniques such as Symbolic Execution are gaining notority in this domain, one of those is Bounded Model Checking (BMC). BMC is a verification technique that encodes a property in paths of transition system up to a bound k to one single logic formula such that if the system contains a flaw the formula will generate a proof. This proof contain information for the testcase generation. The difficult of using BMC for testcase is at the time/space complexity and at the optimizations trying to workaround this issue. Incremental BMC is a strategy that increases the k limit until the violation is found or the system is completely verified. The issue is that at each increment every path is verified again, which add time and memory consuption to solve the current instance. To solve those issue this work proposes two main contributions: (1) algorithm for testcase generation using proofs; and (2) a caching system that uses small instances by: (A) direct use; and (B) indirect use of other systems. Those contributions were implemented into the Efficient SMT-based Bounded Model Checker (ESBMC), being tested over Continuos Integration and over public benchmarks of C programs, obtaining the first place at TestComp???21 in the Cover-error category and reducing the time of the CI. A gera????o autom??tica de casos de teste consiste na gera????o de entradas para um algoritmo que sejam capazes de explorar todos os caminhos de um programa, maximizando a cobertura. Comumente, t??cnicas como fuzzing s??o utilizadas para isso por sua performance alta e de custo baixo. Entretanto, t??cnicas formais, como execu????o simb??lica, v??m ganhando espa??o nesse dom??nio, entre elas, a Bounded Model Checking (BMC). BMC ?? uma t??cnica de verifica????o que codifica uma propriedade em caminhos de um sistema de transi????o at?? um limite k, resultando em uma ??nica f??rmula l??gica que, caso contenha uma viola????o, ir?? gerar uma prova. Essa prova - embora reduzida - cont??m informa????es que podem ser utilizadas como base para a gera????o de um caso de teste. A dificuldade de usar BMC em casos de teste est?? na complexidade de tempo/espa??o da t??cnica e nas simplifica????es feitas para tentar contornar isso (simplifica????es, estrat??gias). Incremental BMC ?? uma estrat??gia que, de forma incremental, aumenta esse limite k at?? que uma viola????o seja encontrada ou que o sistema seja completamente verificado. Entretanto, cada caminho do sistema ?? reverificado a cada incremento, o que adiciona tempo e consumo de mem??ria para resolver a inst??ncia atual. Para resolver esses problemas, este trabalho prop??e duas contribui????es: (1) algoritmo de gera????o de casos de teste a partir de provas e (2) um sistema de cache que utiliza solu????es de inst??ncias menores atrav??s de (A) uso direto das inst??ncias anteriores; e (B) uso indireto atrav??s de f??rmulas de outros sistemas. Essas contribui????es foram implementadas no Efficient SMT-based Bounded Model Checker (ESBMC), sendo testadas em situa????es de Integra????o Cont??nua (CI) e sobre benchmarks p??blicos de programas em C, obtendo a primeira coloca????o na competi????o TestComp???21 na categoria reach-error e reduzindo o tempo do CI.

No âmbito do desenvolvimento de aplicações web têm surgido novos paradigmas para acompanhar a evolução dos diferentes perfis de utilizadores que acedem à Internet, originando novos desafios a ter em consideração na aplicação a desenvolver. Dessa forma, é necessário prever algumas circunstâncias (por exemplo, as características do utilizador como indivíduo, as características do dispositivo) e ambientes específicos (por exemplo, o espaço físico em que o utilizador se encontra). Surge o conceito de PWA (Progressive Web App) que introduz uma nova arquitetura de desenvolvimento com novas propriedades esperadas na aplicação desenvolvida. Este trabalho tem como principal objetivo estudar de uma forma detalhada o funcionamento do sistema de Caching, o qual constitui uma das principais características de uma PWA. Pretende-se abordar os diferentes tipos de caching usados quer numa aplicação web mais tradicional quer numa PWA. Serão também estudadas algumas métricas para avaliar o desempenho em que o sistema de caching tenha influência. De forma a facilitar a compreensão do processo de criação de uma aplicação web que respeita as sugestões de uma PWA, será também considerado o caso de estudo de uma aplicação web, para a qual será considerada uma versão web mais tradicional, e uma outra seguindo as sugestões de uma PWA (em particular o desenvolvimento dos service workers, componentes fundamentais no comportamento da cache das PWA). É realizado um estudo comparativo do desempenho das duas diferentes versões da aplicação, tendo em conta diferentes métricas sugeridas, tais como: “First Contentful Paint”, “Speed Index”, “Time to Interactive”, “First Meaningful Paint”, “First CPU Idle” e “Max Potential First Input Delay”.

Submitted by JOSIANE SANTOS DE OLIVEIRA (josianeso) on 2018-05-11T12:40:43Z No. of bitstreams: 1 Felipe Rabuske Costa_.pdf: 3408830 bytes, checksum: 25a67ecb02629c811b5f305a1f2e3d27 (MD5) Made available in DSpace on 2018-05-11T12:40:43Z (GMT). No. of bitstreams: 1 Felipe Rabuske Costa_.pdf: 3408830 bytes, checksum: 25a67ecb02629c811b5f305a1f2e3d27 (MD5) Previous issue date: 2018-02-28 Nenhuma Estima-se que até o ano de 2020, cerca de 50 bilhões de dispositivos móveis estarão conectados a redes sem fio e que 78% de todo o tráfego de dados gerado por esse tipo de dispositivos será conteúdo multimídia. Essas estimativas fomentam o desenvolvimento da quinta geração de redes móveis (5G). Uma das arquiteturas mais recentemente proposta, chamada de Fog Radio Access Networks (F-RAN), dá aos componentes localizados na borda da rede poder de processamento e armazenamento endereçados às atividades da rede. Um dos principais problemas dessa arquitetura é o intenso tráfego de dados no seu canal de comunicação centralizado chamado fronthaul, utilizado para conectar as antenas (F-APs) à rede externa. Dado esse contexto, esse trabalho apresenta o Nuoxus, um modelo de caching de conteúdo multimídia voltado para F-RANs que visa amenizar esse problema. Ao armazenar esse tipo de conteúdo nos nós de rede mais próximos ao usuário, o número de acessos concorrentes ao fronthaul é reduzido, sendo esse um dos fatores agravantes na latência de comunicação na rede. O Nuoxus pode ser executado em qualquer nó da rede que possua capacidade de armazenamento e processamento, ficando responsável por gerenciar o caching de conteúdo desse nó. Sua política de substituição de conteúdo utiliza a similaridade de requisições entre os nós filhos e o restante da rede como um fator para definir a relevância de armazenar o conteúdo requisitado em cache. Além disso, utilizando esse mesmo processo, o Nuoxus sugere, de forma proativa, aos demais nós filhos que apresentam um alto grau de similaridade que façam o caching desse conteúdo, visando um possível futuro acesso. A análise do estado da arte demonstra que até o momento não existe nenhum outro trabalho que explore o histórico de requisições para fazer caching de conteúdo em arquiteturas multicamadas para redes sem fio de forma proativa e sem utilizar algum componente centralizado para fazer coordenação e predição de caching. A fim de comprovar a eficiência do modelo, foi desenvolvido um protótipo utilizando o simulador ns-3. Os resultados obtidos demostram que a utilização do Nuoxus foi capaz de reduzir a latência de rede em cerca de 29.75%. Além disso, quando comparado com outras estratégias de caching, o número de acesso à cache dos componentes de rede aumentou em 53.16% em relação à estratégia que obteve o segundo melhor resultado. It is estimated that by the year 2020, about 50 billion mobile devices will be connected to wireless networks and 78% of the data traffic of this kind of device will be multimedia content. These estimates foster the development of the 5th generation of mobile networks (5G). One of the most recently proposed architectures, named Fog Radio Access Networks or F-RAN, gives the components located at the edge of the network the processing power and storage capacity to address network activities. One of the main problems of this architecture is the intense data traffic in its centralized component named fronthaul, which is used to connect the antennas (FAPs) to the external network. Given this context, we propose Nuoxus, a multimedia content caching model for F-RANs that aims to mitigate this problem. By storing the content in the nodes closest to the user, the number of concurrent accesses to the fronthaul is reduced, which decreases the communication latency of the network. Nuoxus can run on any network node that has storage and processing capacity, becoming the responsible for managing the cache of that node. Its content replacement policy uses the similarity of requests between the child nodes and the rest of the network as a factor to decide the relevance of storing the requested content in the cache. Furthermore, by using this same process, Nuoxus proactively suggests to the child nodes whose degree of similarity is high to perform the caching of the content, assuming they will access the content at a future time. The State-of-the-art analysis shows that there is no other work that explores the history of requests to cache content in multi-layer architectures for wireless networks in a proactive manner, without using some centralized component to do coordination and prediction of caching. To demonstrate the efficiency of the model, a prototype was developed using the ns 3 simulator. The results obtained demonstrate that the use of Nuoxus reduced network latency in 29.75%. In addition, when compared to other caching strategies, the cache hit increased by 53.16% when compared to the strategy that obtained the second-best result.

Um desafio fundamental em ICN (do inglês Information-Centric Networking) é desenvolver Content Stores (ou seja, unidades de cache) que satisfaçam três requisitos: espaço de armazenamento grande, velocidade de operação rápida e custo acessível. A chamada Hierarchical Content Store (HCS) é uma abordagem promissora para atender a esses requisitos. Ela explora a correlação temporal entre requisições para prever futuras solicitações. Por exemplo, assume-se que um usuário que solicita o primeiro minuto de um filme também solicitará o segundo minuto. Teoricamente, essa premissa permitiria transferir proativamente conteúdos de uma área de cache relativamente grande, mas lenta (Layer 2 - L2), para uma área de cache mais rápida, porém menor (Layer 1 - L1). A estrutura hierárquica tem potencial para incrementar o desempenho da CS em uma ordem de grandeza tanto em termos de vazão como de tamanho, mantendo o custo. Contudo, o desenvolvimento de HCS apresenta diversos desafios práticos. É necessário acoplar as hierarquias de memória L2 e L1 considerando as suas taxas de transferência e tamanhos, que dependem tanto de aspectos de hardware (por exemplo, taxa de leitura da L2, uso de múltiplos SSD físicos em paralelo, velocidade de barramento, etc.), como de software (por exemplo, controlador do SSD, gerenciamento de memória, etc.). Nesse contexto, esta tese apresenta duas contribuições principais. Primeiramente, é proposta uma arquitetura para superar os gargalos inerentes ao sistema através da paralelização de múltiplas HCS. Em resumo, o esquema proposto supera desafios inerentes à concorrência (especificamente, sincronismo) através do particionamento determinístico das requisições de conteúdos entre múltiplas threads. Em segundo lugar, é proposta uma metodologia para investigar o desenvolvimento de HCS explorando técnicas de emulação e modelagem analítica conjuntamente. A metodologia proposta apresenta vantagens em relação a metodologias baseadas em prototipação e simulação. A L2 é emulada para viabilizar a investigação de uma variedade de cenários de contorno (tanto em termos de hardware como de software) maior do que seria possível através de prototipação (considerando as tecnologias atuais). Além disso, a emulação emprega código real de um protótipo para os outros componentes do HCS (por exemplo L1, gerência das camadas e API) para fornecer resultados mais realistas do que seriam obtidos através de simulação. A key challenge in Information Centric Networking (ICN) is to develop cache units (also called Content Store - CS) that meet three requirements: large storage space, fast operation, and affordable cost. The so-called HCS (Hierarchical Content Store) is a promising approach to satisfy these requirements jointly. It explores the correlation between content requests to predict future demands. Theoretically, this idea would enable proactively content transfers from a relatively large but slow cache area (Layer 2 - L2) to a faster but smaller cache area (Layer 1 - L1). Thereby, it would be possible to increase the throughput and size of CS in one order of magnitude, while keeping the cost. However, the development of HCS introduces several practical challenges. HCS requires a careful coupling of L2 and L1 memory levels considering their transfer rates and sizes. This requirement depends on both hardware specifications (e.g., read rate L2, use of multiple physical SSD in parallel, bus speed, etc.), and software aspects (e.g., the SSD controller, memory management, etc.). In this context, this thesis presents two main contributions. First, we propose an architecture for overcoming the HCS bottlenecks by parallelizing multiple HCS. In summary, the proposed scheme overcomes racing condition related challenges through deterministic partitioning of content requests among multiple threads. Second, we propose a methodology to investigate the development of HCS exploiting emulation techniques and analytical modeling jointly. The proposed methodology offers advantages over prototyping and simulation-based methods. We emulate the L2 to enable the investigation of a variety of boundary scenarios that are richer (regarding both hardware and software aspects) than would be possible through prototyping (considering current technologies). Moreover, the emulation employs real code from a prototype for the other components of the HCS (e.g., L1, layers management and API) to provide more realistic results than would be obtained through simulation.

Dissertação de mestrado em Engenharia Informática, Neste projeto de investigação, abordar-se-á o desempenho de vários algoritmos de caching em Redes Tolerantes a Atrasos com Dados Nomeados. Os algoritmos de caching são fundamentais para o armazenamento e distribuição dos conteúdos nos nós. É utilizado como ponto de partida os algoritmos de caching das Redes Tolerantes a Atrasos e Redes de Dados Nomeados, e igualmente nas redes IP tradicionais e web proxies. Com base nesses conhecimentos, serão introduzidas alterações no sentido de os adaptar ao contexto proposto dos mecanismos de Redes de Dados Nomeados em Redes Tolerantes a Atrasos. Em termos experimentais será usado o ambiente de simulação ICONE (Information Centric Opportunistic Networking Environment) desenvolvida com base no ONE (Opportunistic Networking Environment), um simulador para Redes Tolerantes a Atrasos. O ICONE introduz extensões de suporte a Redes de Dados Nomeados no ONE. Os algoritmos serão avaliados pela sua probabilidade de interesses satisfeitos, latência de interesses satisfeitos, interesses encaminhados, sobrecarga da rede, entre outros. Serão usados parâmetros como espaço de armazenamento para a cache, tempo de simulação, ritmo de geração de interesses entre outros. São também importantes aspetos como a segurança, confiabilidade e escalabilidade dados., The importance of communication in our actual civilization causes a constant search for solutions able to solve existing problems. Areas where communications are intermittent, constitute one of these problems. Through a Delay Tolerant Network it is possible to communicate more efficiently and reliably. Their ability to data caching can store the contents on all nodes through which they travel. This enables better resilience to failures and delays. The ability to run other technologies on NDN, makes possible the coexistence with the Named Data Networking. These were developed in order to replace the traditional IP networks. NDN claims that an architecture based on host-to-host communications like the current Internet, it is not suitable for network user patterns. Instead, NDN use names for each existing content on the network and allows interest generation on a particular content that the network will send back. Each node is capable of data caching and this allows it to respond with the corresponding content, when a cache hit occurs. Due to the good coexistence between DTNs and NDNs, there are several network architectures and joining these two technologies. They use the data caching as a way to increase performance and network resiliency. For this reason, the study of caching is a very important issue. The goal of this thesis is the study of several algorithms and mechanisms for caching on Named Data Delay Tolerant Networks. Then, using the ICONE testbed, these algorithms were simulated and evaluted using several metrics namely percentages of satisfied interests, cache hits and computational efforts to complete the process. Results show significant improvements in the percentage of satisfied interest when using caching algorithms, in particular with the Network Interest algorithm. Results improve with the usage of repository components (Repo) architectures.

Submitted by João Silva (jpps@estgf.ipp.pt) on 2018-03-12T17:34:38Z No. of bitstreams: 1 DM_ArmindoPereira_MEI_2011.pdf: 3063808 bytes, checksum: 4018a1b686ad594bf1cbbe38d26275cc (MD5) Made available in DSpace on 2018-03-12T17:34:38Z (GMT). No. of bitstreams: 1 DM_ArmindoPereira_MEI_2011.pdf: 3063808 bytes, checksum: 4018a1b686ad594bf1cbbe38d26275cc (MD5) Previous issue date: 2011