Submitted by Renata Lopes (renatasil82@gmail.com) on 2017-08-24T17:59:29Z No. of bitstreams: 1 brunomarquescremonezi.pdf: 4447666 bytes, checksum: aa9f96e265197cfc5a70f8dfc8ad53ad (MD5) / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2017-08-25T12:03:47Z (GMT) No. of bitstreams: 1 brunomarquescremonezi.pdf: 4447666 bytes, checksum: aa9f96e265197cfc5a70f8dfc8ad53ad (MD5) / Made available in DSpace on 2017-08-25T12:03:47Z (GMT). No. of bitstreams: 1 brunomarquescremonezi.pdf: 4447666 bytes, checksum: aa9f96e265197cfc5a70f8dfc8ad53ad (MD5) Previous issue date: 2017-06-02 / FAPEMIG - Fundação de Amparo à Pesquisa do Estado de Minas Gerais / O aumento do uso de redes sem fios e a constante miniaturização dos dispositivos permitiram o desenvolvimento das redes de sensores corporais sem fio (do inglês, wireless body area networks — WBANs). Nessas redes, diversos sensores são posicionados sobre ou sob a pele do usuário. Os sensores de uma WBAN coletam dados sobre batimentos cardíacos, temperatura corporal ou até mesmo um prolongado cardiograma. Através do uso de WBAN, os usuários terão um monitoramento não invasivo e que pouco afeta a sua mobilidade. Essas características, no entanto, abrem portas para diversos problemas. Por transmitir informações críticas, a comunicação é sensível à latência e à perda de pacotes. De fato, alta latência e perda de dados vitais podem acarretar em sérias consequências na vida dos pacientes e, em casos extremos, levando ao óbito. As características inerentes em uma comunicação sem fio geram problemas para redes corporais. Com sua popularização e alta mobilidade, é razoável considerar a existência de ambientes médicos muito densos, em que duas ou mais redes corporais podem utilizar simultaneamente o mesmo canal de comunicação sem fio. Essa situação potencializa as interferências, acarretando um maior número de retransmissões e perdas de pacotes, e, consequentemente, levando a um aumento da latência. Diante disso, este trabalho apresenta o PDAC (Protocol for Dynamic Channel AlioCation), um protocolo para alocação dinâmica de canais, ciente dos requisitos de aplicações médicas. O PDAC oferece uma solução para reduzir interferências entre redes corporais sem fio tirando proveito da arquitetura de um ambiente hospitalar. No PDAC, diversas estações base trabalham de forma colaborativa para atender aos requisitos das aplicações médicas. Para uma alocação livre de interferências, o PDAC é inspirado por uma solução gulosa de um problema de coloração de grafos, oferecendo meios para evitar que estações base vizinhas utilizem o mesmo canal simultaneamente. Além disso, o PDAC oferece, através da agregação de canais, melhores vazões. A avaliação de desempenho do PDAC foi realizada em duas fases: por meio de experimentos de simulação e análises formais. Os resultados de simulação indicam que, em um ambiente médico realista, o PDAC é capaz de em média aumentar a vazão em 30% e reduzir a latência em 40%, quando comparado com protocolos de alocação de frequência do estado da arte. A outra fase consiste na verificação formal que por sua vez mostrou a coerência do protocolo e que o mesmo satisfaz todas as propriedades de segurança verificadas. / The increased use of wireless networks and the constant miniaturization of devices allowed the development of wireless body area networks (WBANs). In these networks, diverse sensors are positioned on the user's skin. The sensors in a WBAN gather data from heart rate, body temperature or even a cardiogram. Through the use of WBAN, patients will have a noninvasive monitoring system, which hardly affects their mobility. These characteristics, however, create several problems. By transmitting critical informa-tion, these data are quite sensitive to high latency and packet loss. The loss of vital data can lead to serious consequences in the users' life and, in extreme cases, leading to death. The inherent characteristics of wireless communication are a major issue for WBANs. With their popularization and high mobility, it is reasonable to consider the existence of very dense medical environments, where two or more WBANs can simultaneously use the same wireless communication channel. This situation can produce interference, leading to a bigger number of retransmissions and packet losses, and consequently increasing latency. Therefore, this master thesis presents the PDAC (Protocol for Dynamic Channel AlloCation), a protocol for dynamic channel allocation, that is aware of the requirements of medical applications. PDAC offers a solution to reduce interference between WBANs by taking advantage of the architecture of a hospital environment. Using PDAC, several base stations work collaboratively to meet medical application requirements. For an interference-free allocation, PDAC is inspired by a greedy solution of a graph colouring problem, preventing neighbouring base stations of using the same channel simultaneously. In addition, PDAC offers through the channel bonding, a better goodput. The evaluation PDAC was performed in two phases: by means of simulations and formal analysis. Simulation results indicate that PDAC is able to increase goodput by 30% (on average) and reduce latency by 40% (on average) when compared to the literature. The formal verification, in turn, shows that the protocol is consistent and also satisfies all verified security properties.