Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Engenharia Elétrica. / Made available in DSpace on 2012-10-18T20:18:42Z (GMT). No. of bitstreams: 0Bitstream added on 2016-01-09T02:25:30Z : No. of bitstreams: 1 193147.pdf: 7504038 bytes, checksum: a7fe9d95e293c9b051a546c2b13d3c37 (MD5) / A utilização de ferramentas de verificação formal em sistemas de comunicação de dados é um tema que contem diversos tópicos de pesquisa que estão constantemente recebendo o ingresso de novos estudos. Apesar da essência do conceito de verificação formal já estar fundamentada, novas metodologias, técnicas, estratégias e ferramentas estão sendo desenvolvidas a cada dia, tornando a verificação formal cada vez mais próxima e adequada à utilização por projetistas que desenvolvem sistemas, tais como os de comunicação de dados. O mito de que as ferramentas de verificação formal estão restritas ao meio acadêmico, onde apenas matemáticos estariam aptos a utilizá-las, pode ser desmistificado com trabalhos que mostram como uma pessoa que conhece um sistema pode tirar proveito da verificação formal para identificar erros. Este trabalho nasceu em torno deste objetivo, mostrando características das metodologias e ferramentas de verificação, e como elas podem ser aplicadas num sistema de comunicação de dados. O trabalho foi dividido em capítulos inter-relacionados. No capitulo 1 trabalham-se os principais conceitos relacionados ao tema. No capítulo 2 apresentam-se as vantagens e desvantagens da verificação formal sobre a simulação. São mostrados alguns métodos aplicáveis na verificação formal, tecendo algumas considerações e comparações entre eles. Mostra-se o poder da Checagem de Modelos e suas aplicações, introduzindo o capítulo 3. Neste capítulo trabalham-se detalhes da Checagem de Modelos, mostrando como é feita a verificação através desta metodologia e apresentando seus maiores problemas, como a explosão de estados, e as principais soluções, além de mostrar como se utilizam as especificações através de Lógicas Temporais. Apresentam-se também as principais ferramentas de Checagem de Modelo do mercado, o SPIN e o SMV, introduzindo o capítulo 4. Neste são mostradas algumas características especificas da ferramenta SMV, que será utilizada na análise de um sistema padronizado pelo ATM Forum. Durante todo o capítulo a ênfase é dada sobre o SMV, porém, ao invés de abrir um capítulo para a solução SPIN, esta ferramenta é comparada com o SMV ao longo da exposição. No capítulo 5 apresentam-se as principais características a serem consideradas na verificação de protocolos de comunicação de dados. Através da utilização do modelo OSI como filosofia buscou-se abranger qualquer protocolo. Entretanto houve a necessidade de se mostrar algumas características próprias do sistema a ser discutido, o ATM, que é apresentado no capitulo 6. Durante todo este capitulo mostraram-se características do ATM, que é um sistema de comunicação de dados relativamente simples que tira proveito das baixas taxas de erros dos modernos sistemas de transmissão. Dentro do universo de diferentes aplicações suportadas pelo ATM focou-se num aspecto específico, o gerenciamento de tráfego, que é trabalhado dentro do capítulo 7, utilizando-se da ferramenta SMV para verificação de projetos. O trabalho conclui no capitulo 8 com as recomendações e conclusões propriamente ditas.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Engenharia Elétrica. / Made available in DSpace on 2013-07-15T23:04:17Z (GMT). No. of bitstreams: 1 229659.pdf: 1022907 bytes, checksum: ff363db3b6597596eab67c4e735946b7 (MD5) / Neste trabalho, é apresentado um simulador de ruídos impulsivos assíncronos, os quais estão presentes nos sistemas de transmissão de dados pela rede de distribuição de energia elétrica (PLC - Power Line Communications). O simulador leva em conta tanto as características temporais como as espectrais do ruído impulsivo e baseia-se nos métodos de Mann et al., para sistemas xDSL (Digital Subscriber Line), e de Degardin et al. As estatísticas dos parâmetros modelados são derivadas de observações de ruído impulsivo na rede de energia elétrica de um dos laboratórios do Instituto de Eletrônica de Potência (INEP) da Universidade Federal de Santa Catarina (UFSC). Apesar de serem utilizadas apenas 68 observações, os resultados de simulação permitem comprovar que o sistema de modelagem e simulação proposto pode ser usado na geração de ruído impulsivo assíncrono para testar as técnicas de modulação e codificação de canal dos sistemas PLC.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. / Made available in DSpace on 2012-10-21T09:52:19Z (GMT). No. of bitstreams: 1 201486.pdf: 496463 bytes, checksum: 55424db49c821ad081991d52c7ee8aa5 (MD5) / Esta dissertação aborda o problema de escalonamento sob restrições de recursos em Síntese de Alto Nível. Tradicionalmente, os algoritmos de escalonamento associam operações a instantes de tempo, levando em conta um número pré-fixado de unidades funcionais (somadores, ALUs, multiplicadores). Entretanto, para viabilizar a execução de uma operação em uma unidade funcional, os operandos precisam ser preliminarmente lidos de registradores e transportados, através de barramentos, até as entradas da unidade funcional. Além disso, o resultado da operação precisa também ser transportado, através de um barramento, até o registrador destino. Conseqüentemente, o escalonamento de muitas operações em paralelo pode levar à alocação de um número proibitivo de barramentos. Isto torna desejável que um algoritmo de escalonamento seja capaz de manipular também restrições impostas por um número pré-fixado de barramentos. Este trabalho estende um algoritmo de escalonamento clássico, usando a noção de transferência entre registradores (RT) ao invés da simples noção de operação. Assim, o escalonador estendido torna-se capaz de manipular, além das restrições de precedência, restrições de recursos impostas por um número limitado de recursos, sejam eles unidades funcionais e/ou barramentos. Resultados experimentais mostram o impacto do número limitado de barramentos sobre a latência.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. / Made available in DSpace on 2012-10-19T22:52:45Z (GMT). No. of bitstreams: 1 188792.pdf: 1822327 bytes, checksum: 20143a744be235b45757fb6a1829124e (MD5) / O desenvolvimento das telecomunicações e da informática, nos últimos anos unido à necessidade do homem de estar cada vez mais informado esteja onde estiver, tem provocado que as redes wireless sejam a próxima geração nas redes de computadores. As redes Wireless, surgem como a quarta revolução na computação, antecedida pelos centros de processamento de dados na década de sessenta, o surgimento dos terminais nos anos setenta e das redes de computadores na década de oitenta. A evolução conjunta da comunicação sem fio e da tecnologia da informática busca atender muitas das necessidades do mercado: serviços celulares, redes locais sem fio, transmissões de dados via satélites, TV, rádio modem, sistemas de navegação, base de dados geográfica. A combinação da comunicação sem fio com a mobilidade de computadores criou novos problemas nas áreas de informática e telecomunicações, em especial, com o problema de interferências entre equipamentos transmissores/receptores pela padronização não estar completamente pronta. Este dissertação procura concentrar através de uma revisão da literatura juntamente com implementações de outras tecnologias, mostrando uma solução alternativa para os problemas de colisões da tecnologia Spread Spectrum.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação / Made available in DSpace on 2012-10-17T10:49:34Z (GMT). No. of bitstreams: 1 224776.pdf: 1645264 bytes, checksum: f05448e68efe1dd5d8fa0e14a6d86126 (MD5) / Este trabalho descreve exatamente a tecnologia spread spectrum (SS) funcionando inicialmente na banda de 902-928 MHz e posteriormente estendendo-se para as faixas de 2.4 e 5.8 GHz, consolidando, pelos organismos internacionais reguladores de telecomunicações, a banda ISM (Industrial Scientific and Medical) ou ICM (Indústria Ciência e Medicina) no Brasil, a qual constitui uma banda especial, específica, licenciada e livre para as áreas abrangentes de suas próprias definições. Contudo, não implica que esta banda seja utilizada por diversas empresas de vários segmentos comerciais.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação / Made available in DSpace on 2012-10-17T12:44:36Z (GMT). No. of bitstreams: 0Bitstream added on 2014-09-25T17:21:26Z : No. of bitstreams: 1 180012.pdf: 7574793 bytes, checksum: 15fea0b9f793cacd7e6f3b297ee342da (MD5) / No cenário atual de telecomunicações no Brasil as empresas operadoras estão migrando de um ambiente onde até recentemente as definições estratégicas de desenvolvimentos de novos serviços e de investimentos na rede de telecomunicações eram de responsabilidade da engenharia. Numa arena de competição, o mercado começa a exercer este papel eo cliente é o foco principal. A princípio o que parece ser fácil e óbvio de imlementar, encontra obstáculos pela dificuldade em visualizar de forma integrada os processos voltados à área de serviços de telecomunicações. O trabalho propõe um modelo, especificado na linguagem UML, para permitir uma visão de gerência do processo de aprovisionamento de serviços de comunicação de dados. Uma vez identificados os principais ofensores do processo atual de designação de facilidades e propondo uma visão integrada dos processos desenvolveu-se um modelo de avaliação de desempenho do processo de designação de facilidades. A modelagem, implementada no Arena Business Process, permite avaliar o impacto dos novos processos no tempo final do aprovisionamento.