Submitted by Geyciane Santos (geyciane_thamires@hotmail.com) on 2015-07-15T15:28:00Z No. of bitstreams: 1 Dissertação - Luiz Filipe da Silva Souza Pinto.pdf: 1522640 bytes, checksum: a54871524028e554440a39db821f0f39 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-20T14:41:25Z (GMT) No. of bitstreams: 1 Dissertação - Luiz Filipe da Silva Souza Pinto.pdf: 1522640 bytes, checksum: a54871524028e554440a39db821f0f39 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-20T14:44:33Z (GMT) No. of bitstreams: 1 Dissertação - Luiz Filipe da Silva Souza Pinto.pdf: 1522640 bytes, checksum: a54871524028e554440a39db821f0f39 (MD5) / Made available in DSpace on 2015-07-20T14:44:33Z (GMT). No. of bitstreams: 1 Dissertação - Luiz Filipe da Silva Souza Pinto.pdf: 1522640 bytes, checksum: a54871524028e554440a39db821f0f39 (MD5) Previous issue date: 2012-12-23 / Não Informada / Digital TV is increasingly present in the lives of Brazilians, because year after year, a large number of people are migrating from analog to digital as the analog system has a date for its shutdown. With the advancement of digital TV, you may notice significant improvements in audio and video technology used, it is also possible to establish an interaction between the viewer and the TV receiver device. In Brazil, this interaction occurs through the Ginga middleware technology developed by Brazilian researchers to standardize the interactive content sent to devices able to interpret it. In addition to televisions, another popular device is the mobile phone, which is present in a significant way across the country. The technology adopted by Brazil for the digital transmission of television signals, allows the phone to receive programming dedicated to portable devices in open and free way. The phone has a certain advantage over television due to its connectivity. Once the mobile phone is on most of the time connected to a telephone network, and may be 2G, 2.5G, 3G and 4G in the near future, while the television set is for the most part of the time offline (disconnected). This work presents a proposal to use the SMS service as interactive channel, also known as the return channel, for portable reception. This service is present in all mobile phones, and therefore may contribute to the popularization of the use of digital TV technology in the country. / A TV digital está cada vez mais presente na vida dos brasileiros, pois ano após ano, um número grande de pessoas está migrando do sistema analógico para o digital, uma vez que o sistema analógico tem data certa para seu encerramento. Com o avanço da TV digital, é possível notar melhoras significativas nas tecnologias de áudio e vídeo usadas, como também é possível estabelecer uma interação entre o telespectador e o dispositivo receptor. No Brasil, tal interação ocorre através do middleware Ginga, tecnologia desenvolvida por pesquisadores brasileiros para padronizar o conteúdo interativo enviado aos dispositivos capazes de interpretá-lo. Além dos televisores, outro dispositivo bastante popular é o telefone celular, que está presente de forma expressiva ao longo do país. A tecnologia adotada pelo Brasil para transmissão digital do sinal de TV, permite que o telefone celular receba a programação dedicada a dispositivos portáteis de formaaberta e gratuita. O telefone celular possui uma certa vantagem em relação ao aparelho de televisão no quesito conectividade. Uma vez que o telefone celular está na maior parte do tempo conectado a uma rede de telefonia, podendo ser 2G, 2.5G, 3G e em um futuro próximo 4G, enquanto que o aparelho de televisão está em sua maior parte do tempo offline (desconectado). Este trabalho apresenta uma proposta para o uso do serviço de SMS como canal de interatividade, também conhecido como canal de retorno, para recepção portátil. Este serviço está presente em todos os telefones celulares, e por isso, pode contribuir para a popularização do uso da tecnologia de TV digital no país.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-12-03T20:22:30Z No. of bitstreams: 1 Dissertação_Luiz_Sales_Silva.pdf: 4959512 bytes, checksum: 383643b6b730dee5b618ea14f782267d (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-12-04T12:28:16Z (GMT) No. of bitstreams: 1 Dissertação_Luiz_Sales_Silva.pdf: 4959512 bytes, checksum: 383643b6b730dee5b618ea14f782267d (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-12-04T12:35:43Z (GMT) No. of bitstreams: 1 Dissertação_Luiz_Sales_Silva.pdf: 4959512 bytes, checksum: 383643b6b730dee5b618ea14f782267d (MD5) / Made available in DSpace on 2015-12-04T12:35:43Z (GMT). No. of bitstreams: 1 Dissertação_Luiz_Sales_Silva.pdf: 4959512 bytes, checksum: 383643b6b730dee5b618ea14f782267d (MD5) Previous issue date: 2014-05-14 / FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas / Currently, the problem of detention fiducial points on human faces has received increasing attention from the scientific community. Recently, we may find in the literature developed some systems for the purpose of performing detecçiia fiducial points. Some of these representatives use clasSifieadows SVM. One of the problems faced by this. fano approach is that the performance of SVM classifiers is extremely sensitive to change its parameters. list is a difficulty that is not trivial to exploit. In this lecture tion, we propose a fiducial points detection system, which uses SVM classifiers, in order to investigate the performance of the classifiers for con-along pre-defined parameters. With this investiwida, we intend to describe the system's behavior to the set of parameters and determine what the parameters = bination, and its values, which produces the best pos-sible performance for the branch system a whole. The proposed system is complex due to. lot of steps involved. The measured performance of the proposed system was performed. for. eleven Aduri tips: ais of. human face. two bases of image data (BiolD and End). The results demonstrate that the system performance. proposed is incremented when using the approach adopted. The system performance is satisfactory when compared with similar systems. / Atualmente, o problema da detenção de pontos fiduciais em faces humanas vem recebendo crescente atenção da comunidade científica. Recentemente, podemos encontrar na literatura alguns sistemas desenvolvidos com o objetivo de realizar a detecçiia de pontos fiduciais. Alguns destes representantes utilizam clasSifieadows SVM. Um dos problemas enfrentados por essa abordagem reside no fato de que o desempenho das clasSificadores SVM é extremamente sensível à mudança de seus parâmetros. lista é uma dificuldade que não é trivial de se explorar. Nesta dissertar ção, propomos um sistema de detecção de pontos fiduciais, que utiliza clasSificadores SVM, com o objetivo de investigar o desempenho dos classificadores para um con-junto de parâmetros pré-definidos. Com esta investiwida, pretendemos descrever o comportamento do sistema para o conjunto de parâmetros e determinar qual é a =binação de parâmetros, e de seus valores, que produz o melhor desempenho pos-sível para o sistema ramo um todo. O sistema proposta é complexo devido a. grande quantidade de etapas envolvidas. A avaliada de desempenho do sistema proposto foi realizada. para. onze pontas Aduri:ais da. face humana para. duas bases de dados de imagens (BiolD e Fim). O resultados demonstram que o desempenho do sistema. proposto é incrementado quando utilizamos a abordagem adotada. O desempenho do sistema é satisfatório quando comparado com os de sistemas similares.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-01-26T20:27:25Z No. of bitstreams: 1 Dissertação - Rafaelli Pereira de Souza.pdf: 3155424 bytes, checksum: 30c412a35e88527a6c1a69eead3c7326 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-01-28T12:39:14Z (GMT) No. of bitstreams: 1 Dissertação - Rafaelli Pereira de Souza.pdf: 3155424 bytes, checksum: 30c412a35e88527a6c1a69eead3c7326 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-01-28T12:40:02Z (GMT) No. of bitstreams: 1 Dissertação - Rafaelli Pereira de Souza.pdf: 3155424 bytes, checksum: 30c412a35e88527a6c1a69eead3c7326 (MD5) / Made available in DSpace on 2016-01-28T12:40:02Z (GMT). No. of bitstreams: 1 Dissertação - Rafaelli Pereira de Souza.pdf: 3155424 bytes, checksum: 30c412a35e88527a6c1a69eead3c7326 (MD5) Previous issue date: 2015-10-02 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The potential for energy efficiency in the industrial sector is quite significant because it is the sector that consumes the most energy in Brazil and worldwide. In recent years, intensified advances in energy efficiency in energy-intensive industries within the global scenario. However, there is still significant potential for global efficiency, especially in emerging economies. In Brazil, the socio-economic development vector of the Amazon is the Industrial Pole of Manaus (PIM). To increase their competitiveness, manufacturers need to optimize their production processes, reducing energy costs and losses. Considering the relationship between efficiency and power quality in productivity and turnover of industries, it is necessary to know how energy is being consumed and the efficiency with which the various segments of the PIM. The objective of this study was to determine the energy efficiency indicators like the specific energy consumption, load factor and average cost of energy as well as the determination of power quality indicators, by analyzing the measured electrical parameters in the main consumer systems of three industries with large representation in the regional scenario. The methodology included field survey, implementation of energy characterization of questionnaires and electrical measurements. The results showed that the industries had indicators of efficiency, for the most part, better than the national average, however, it was found that most consumer industries systems presented disorders related to power quality such as low power factor and harmonic content. Thus, there is a potential for energy efficiency in industrial systems. / O potencial de eficiência energética no setor industrial é bastante significativo, pois é o setor que mais consome energia no Brasil e no Mundo. Nos últimos anos, intensificaram-se os avanços em eficiência energética nas indústrias energo-intensivas dentro do cenário global. No entanto, ainda existe um potencial significativo de eficiência mundial, principalmente nas economias emergentes. No Brasil, o vetor de desenvolvimento socioeconômico da Amazônia é o Polo Industrial de Manaus (PIM). Para aumentar sua competitividade, as indústrias necessitam aperfeiçoar seus processos produtivos, reduzindo perdas de energia e custos. Considerando a relação entre eficiência e qualidade da energia na produtividade e faturamento das indústrias, é necessário conhecer como a energia está sendo consumida e com qual eficiência nos diversos segmentos do PIM. O objetivo deste trabalho foi a determinação dos indicadores de eficiência energética como o consumo específico, fator de carga e custo médio da energia, bem como a determinação dos indicadores de qualidade da energia, através da análise das grandezas elétricas aferidas nos principais sistemas consumidores de três indústrias com grande representação no cenário regional. A metodologia incluiu levantamento de campo, aplicação de questionários de caracterização energética e medições elétricas. Os resultados apontaram que as indústrias apresentaram indicadores de eficiência, na sua maioria, melhores que a média nacional, contudo, foi constatado que grande parte dos sistemas consumidores das indústrias apresentaram distúrbios relacionados a qualidade da energia elétrica, como baixo fator de potência e conteúdo harmônico. Dessa forma, existe um potencial para eficiência energética nos sistemas industriais.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-02-04T15:29:28Z No. of bitstreams: 1 Dissertação -Roberlânio Melo.pdf: 2220610 bytes, checksum: 853fbfde1f919be543e94f5aedf34482 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-02-04T15:29:51Z (GMT) No. of bitstreams: 1 Dissertação -Roberlânio Melo.pdf: 2220610 bytes, checksum: 853fbfde1f919be543e94f5aedf34482 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-02-04T15:30:07Z (GMT) No. of bitstreams: 1 Dissertação -Roberlânio Melo.pdf: 2220610 bytes, checksum: 853fbfde1f919be543e94f5aedf34482 (MD5) / Made available in DSpace on 2016-02-04T15:30:07Z (GMT). No. of bitstreams: 1 Dissertação -Roberlânio Melo.pdf: 2220610 bytes, checksum: 853fbfde1f919be543e94f5aedf34482 (MD5) Previous issue date: 2012-12-14 / Não informada / This dissertation proposes a method of detecting natural gas leak in oil installations, specifically in onshore oil wells, applying pattern recognition techniques in digital images. Other methods of detecting natural gas leak found in the literature, has as its foundation the analysis of methane molecules, applying the catalytic principle or through the absorption of infrared spectrum. These methods have some disadvantages such as reduced service life and conditions of false negatives, respectively. The method of detecting natural gas leak proposed is based on the application of the concept of novelty filter in digital images originated from CCTV. For this, it was tested six different types of novelty filters. The difference between these filters is in the component type of color spaces (RGB or HIS) used in forming the training base of the respective filter. The best component that characterizes a natural gas leak was determined by performance measuring using ROC curves. The results obtained in the filter of novelty R are promising, with maximum sensitivity and specificity equal to 0,969 and 0,961 respectively, and average AUC of 98.527%. / O presente trabalho propõe um método de detecção de vazamento de gás natural em instalações petrolíferas, especificamente em poços onshore, aplicando técnicas de reconhecimento de padrões em imagens digitais. Outros métodos de detecção de vazamento de gás natural encontrados na literatura, têm como fundamento a análise de moléculas de metano, seja aplicando o princípio catalítico ou através da absorção do espectro infravermelho, estes apresentam algumas desvantagens como vida útil reduzida e condições de falsos negativos, respectivamente. O método de detecção de vazamento de gás natural proposto é baseado na aplicação do conceito de filtro de novidade em imagens digitais oriundas do sistema Closed-Circuit Television. Para tanto foram desenvolvidos seis tipos distintos de filtros de novidade, cuja diferença entre estes filtros está no tipo de componente dos espaços de cores RGB ou HSI utilizado na formação da base de treinamento dos respectivos filtros. A melhor componente que caracteriza um vazamento de gás natural foi determinado pelas medidas de desempenho obtidas nas curvas ROC destes filtros de novidade. Os resultados obtidos no filtro de novidade R são promissores, apresentando especificidade e sensibilidade máxima igual a 96,9% e 96,1%, respectivamente e AUC média de 98,527%.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-02-18T18:50:03Z No. of bitstreams: 1 Dissertação - Heitor Judiss Savino.pdf: 12604505 bytes, checksum: fb1bcd22abe6766240e85da3ba2e5109 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-02-18T19:37:30Z (GMT) No. of bitstreams: 1 Dissertação - Heitor Judiss Savino.pdf: 12604505 bytes, checksum: fb1bcd22abe6766240e85da3ba2e5109 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-02-18T19:37:54Z (GMT) No. of bitstreams: 1 Dissertação - Heitor Judiss Savino.pdf: 12604505 bytes, checksum: fb1bcd22abe6766240e85da3ba2e5109 (MD5) / Made available in DSpace on 2016-02-18T19:37:54Z (GMT). No. of bitstreams: 1 Dissertação - Heitor Judiss Savino.pdf: 12604505 bytes, checksum: fb1bcd22abe6766240e85da3ba2e5109 (MD5) Previous issue date: 2012-09-25 / Não informada / Currently, the MPEG-2 transport stream is widely used as multiplexing system for sending audio, video, and data, in digital television networks. The transmitted infor- mation is divided into xed-length pa kets, whi h are multiplexed in time and then sent to the re eiver. In order to ensure the orre t presentation of data related to a given program (e.g., audio and video), the transport stream an provide time bases, whi h are used for syn hronizing the re eption system. However, that information, whi h is known as Program Clo k Referen e (PCR) and is also periodi ally embedded in the multiplexed data stream, may su er from ina ura ies, due to the pro essing hain between transmitter and re eiver, whi h an be per eived in the form of jitter. In order to prevent that errors aused by the transport stream pro essing hain, whi h ompromises the proper presentation of the transmitted information, PCR orre tion methods are normally employed. This work presents a review of the PCR orre - tion methods ommonly used in the literature and introdu es two new ontributions. The rst one onsists of a shared a ess stru ture for the orre tion blo k, whi h has the potential to provide a redu ed omputational omplexity (in terms of arithmeti operations) and hardware requirements, when used with traditional PCR orre tion methods. The se ond one devises an intelligent method for PCR orre tion, whose main feature lies on the redu tion of the jitter aused by the orre tion pro ess. Its ar hite ture is based on the ooperative operation of the main modules involved in this pro ess: the rate adapter and the PCR orre tor. In spite of presenting a higher om- plexity, its superior performan e favors the syn hronization pro ess, performed by the re eiver, whi h makes it suitable for pre ise time-bases demanding systems. The pro- posed methodologies are ombined, whi h provides a omplete and e ient framework for pro essing MPEG-2 transport streams. / Atualmente, o fluxo de transporte MPEG-2 é amplamente utilizado como chamada de transporte para a multiplexação de programas que arregam áudio, vídeo e dados, em redes de televisão digital. As informações transmitidas são divididas em pa otes de tamanho xo, multiplexadas no tempo e então enviadas ao re eptor. Para que os da- dos de um mesmo programa sejam apresentados orretamente e em sin ronismo (e.g. áudio e vídeo), o uxo de transporte permite a in orporação de bases de tempo, que são utilizadas na sin ronização do sistema de re epção. Entretanto, essa informação, onhe ida omo Program Clo k Referen e (PCR) e inserida periodi amente no feixe multiplexado, pode sofrer erros, observados na forma de jitter, devido à adeia de pro- essamento entre transmissor e re eptor. Dessa forma, para se evitar que o erro inserido pelo pro essamento do uxo de transporte prejudique a apresentação da informação enviada, métodos de orreção de PCR são geralmente utilizados. Este trabalho apre- senta um estudo sobre os métodos de orreção de PCR mais utilizados na literatura e introduz duas novas ontribuições. A primeira onsiste em uma estrutura de a esso ompartilhado para o blo o de orreção, que tem o poten ial de propor ionar ara terís- ti as reduzidas de omplexidade omputa ional (quantidade de operações aritméti as) e requisitos de hardware, quando utilizada em onjunto om métodos tradi ionais de orreção de PCR. A segunda onsiste em um método inteligente para a orreção de PCR, uja prin ipal ara terísti a é a redução do erro inserido pelo pro esso de orre- ção. A sua arquitetura é baseada na operação ooperativa dos dois prin ipais agentes envolvidos nesse pro esso: os módulos de adaptação de taxa e de orreção de PCR. Apesar de apresentar maior omplexidade omputa ional, o seu desempenho superior fa ilita o pro esso de sin ronização, exe utado pelo re eptor, o que o torna bastante adequado a sistemas que exigem bases de tempo pre isas. As metodologias propostas são utilizadas em onjunto, propor ionando um esquema integrado e e iente para o pro essamento de uxos de transporte MPEG-2.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-02-18T18:24:40Z No. of bitstreams: 1 Dissertação - Marcus de Lima Braga.pdf: 6450946 bytes, checksum: 146975a14889793868be80d04a6c46c5 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-02-18T19:37:05Z (GMT) No. of bitstreams: 1 Dissertação - Marcus de Lima Braga.pdf: 6450946 bytes, checksum: 146975a14889793868be80d04a6c46c5 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-02-18T19:39:18Z (GMT) No. of bitstreams: 1 Dissertação - Marcus de Lima Braga.pdf: 6450946 bytes, checksum: 146975a14889793868be80d04a6c46c5 (MD5) / Made available in DSpace on 2016-02-18T19:39:18Z (GMT). No. of bitstreams: 1 Dissertação - Marcus de Lima Braga.pdf: 6450946 bytes, checksum: 146975a14889793868be80d04a6c46c5 (MD5) Previous issue date: 2012-01-05 / Não informada / Wireless Sensor Network (WSN) has attracted the interest of researchers in applications development that operate on monitoring and control of physical phenomena, relying on its autonomy and exibility, and on its distributed nature and pervasive. If for one hand, this interest provides the development of new applications, on the other it increases its complexity and therefore costs. This is easily understood due their restrictive features, which make the crucial stages of software development (modeling, veri cation and testing) become a non-trivial task. The programming is carried out very close to the operating system (low level), favoring the distraction in the application of logic and thus requiring more concentration of the developer, as well as technical training, rare among experts. This scenario enables the creation of methodologies and tools that support development on this platform. This study aims to use the formal method called Communicating X-Machine in the construction of WSN applications, o ering an intuitive approach and a modular development, providing to the programmer a higher level of abstraction, making it easier to build applications until the code generation in nesC language programming (TinyOS platform). So, this paper aims to facilitate the development of applications, from their modeling until the code generation, providing to the developer an increase in the level of abstraction, a better understanding of the problem through its partitioning and ease of building WSN applications. / Rede de Sensores Sem Fio (RSSF) tem despertado o interesse de pesquisadores no desenvolvimento de aplicações que atuem no monitoramento e controle de fenômenos físicos, apoiando-se em sua autonomia e exibilidade, e em sua natureza distribuída e pervasiva. Se por um lado, esse interesse proporciona o desenvolvimento de novas aplica- ções, por outro, eleva sua complexidade e consequentemente seus custos. Isto é facilmente entendido devido suas características restritivas, que fazem com que os estágios cruciais do desenvolvimento de software (modelagem, veri cação e testes) se tornem tarefas não triviais. A programação é realizada muito próxima ao sistema operacional (baixo nível), favorecendo a distração na aplicação da lógica e exigindo, portanto, ao desenvolvedor maior concentração, além de formação técnica rara entre os especialistas. Este cenário propicia a criação de metodologias e ferramentas que deem suporte ao desenvolvimento nesta plataforma. Este trabalho tem por objetivo utilizar o método formal Communicating X-Machine na construção de aplicações RSSF, oferecendo uma abordagem intuitiva e um desenvolvimento modular, provendo ao programador elevação no nível de abstração, facilitando a construção de aplicações até a geração de código na linguagem de programa- ção nesC (plataforma TinyOS). Portanto, o presente trabalho pretende facilitar o desenvolvimento de aplicações, desde sua modelagem até a geração de código, proporcionando ao desenvolvedor o aumento no nível de abstração, melhor entendimento do problema através de seu particionamento e facilidade na construção de aplicações em RSSF.

Submitted by Bianca Neves (oliveirabia1@ymail.com) on 2016-04-20T19:50:59Z No. of bitstreams: 1 Dissertação -Hussama Ibrahim Ismail.pdf: 7224207 bytes, checksum: 580676e0f2285e31f50bddf1814c3d9b (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-04-27T18:31:16Z (GMT) No. of bitstreams: 1 Dissertação -Hussama Ibrahim Ismail.pdf: 7224207 bytes, checksum: 580676e0f2285e31f50bddf1814c3d9b (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-04-27T20:06:56Z (GMT) No. of bitstreams: 1 Dissertação -Hussama Ibrahim Ismail.pdf: 7224207 bytes, checksum: 580676e0f2285e31f50bddf1814c3d9b (MD5) / Made available in DSpace on 2016-04-27T20:06:56Z (GMT). No. of bitstreams: 1 Dissertação -Hussama Ibrahim Ismail.pdf: 7224207 bytes, checksum: 580676e0f2285e31f50bddf1814c3d9b (MD5) Previous issue date: 2015-11-11 / Não informada / The extensive use of fixed-point digital controllers demands a growing effort to prevent design errors that appear in discrete-time domain. The present work describes a novel verification methodology, which employs bounded model checking based on boolean satisfiability and satisfiability modulo theories to verify the occurrence of design errors, due to the finite word-length format, in fixed-point digital controllers. Here, the performance of digital controllers realizations that use delta operators are compared to those that use traditional direct forms. Experimental results show that the delta-form realization substantially reduces the digital controllers’ fragility when compared to the direct-form realization. Additionally, the proposed methodology is very effective and efficient to verify real-world digital controllers, where conclusive results are obtained in nearly 89% of the benchmarks. / O uso extensivo de controladores digitais implementados em ponto-fixo demandam um maior esforço para prevenir erros de projeto que aparecem no domínio discreto. Este trabalho descreve uma nova metodologia de verificação que emprega verificação de modelos limitada baseada em satisfação booleana e teorias do módulo da satisfatibilidade, para verificar a ocorrência de erros de projetos em controladores digitais causados pelos efeitos da palavra finita. Neste trabalho, serão comparados os desempenhos das realizações na formas delta e as tradicionais formas diretas. Os resultados mostram que a forma delta reduz substancialmente a fragilidade de controladores digitais, se comparados com as formas diretas. A metodologia proposta é eficiente para verificar controladores digitais do mundo real. Ela foi conclusiva em aproximadamente 89% dos casos de teste.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-06-07T20:26:42Z No. of bitstreams: 1 Dissertação - Robson Silva de Souza.pdf: 3200975 bytes, checksum: 8b96480a153b189d6471670ee9257ef8 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-06-07T20:30:33Z (GMT) No. of bitstreams: 1 Dissertação - Robson Silva de Souza.pdf: 3200975 bytes, checksum: 8b96480a153b189d6471670ee9257ef8 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-06-07T20:34:52Z (GMT) No. of bitstreams: 1 Dissertação - Robson Silva de Souza.pdf: 3200975 bytes, checksum: 8b96480a153b189d6471670ee9257ef8 (MD5) / Made available in DSpace on 2016-06-07T20:34:52Z (GMT). No. of bitstreams: 1 Dissertação - Robson Silva de Souza.pdf: 3200975 bytes, checksum: 8b96480a153b189d6471670ee9257ef8 (MD5) Previous issue date: 2015-09-11 / Não informada / According to Brazilian Institute of Geography and Statistic IBGE – Instituto Brasileiro de Geografia e Estatística (Censo 2010), Brazil has 9.7 million Brazilians with some degree of hearing impairment or deafness, more than five per cent of the population. For the majority of those persons the main natural communication method is the Brazilian Sign Language (LIBRAS – Língua Brasileira de Sinais), instead of the spoken Portuguese. The computer-aided recognition of signs aims to expand the social and digital inclusion of the deaf community by means of those signs translation into audio or text format. This work presents one of the global LIBRAS parameters recognition, the hand gestures, using k-nearest neighbor’s classifier and 2D²PCA dimensionality reduction technique. A robust and representative data set of daily conditions, with 12.200 depth images from 61 hand gesture, captured by Kinect® sensor, was built. Initially the images were segmented in a preprocessing step, which isolated the region of the right hand from the rest of the body. Seeking to eliminate the data set redundancy, the images were submitted to a dimensionality reduction by (2D) dimensional 2PCA technique determining the most representative forms of data from original pixels linear combination. The classifier k-nearest neighbors was the technique in the final stage in the hand gesture automatic recognition. This classifier could correctly categorize 96.31% of test samples (k = 1 and 10x10 feature matrix). Six hand gesture sets were correctly classified obtaining 100% successful rates / De acordo com o IBGE (Censo 2010), o Brasil possui 9,7 milhões de brasileiros com algum grau de deficiência auditiva, mais de cinco por cento da população. Para a maior parte destas pessoas a língua natural principal utilizada para sua comunicação é a LIBRAS (Língua Brasileira de Sinais) e não o português. O reconhecimento de sinais visa permitir uma maior inserção sócio digital da comunidade surda através da interpretação da língua de sinais pelo computador em formato de áudio ou texto. Esta dissertação apresenta o reconhecimento de um dos parâmetros globais da LIBRAS, as configurações de mão, utilizando o classificador k-vizinhos mais próximos e a técnica de redução de dimensionalidade 2D²PCA. Um conjunto de dados, robusto e representativo das condições do cotidiano, constituído de 12.200 imagens de profundidade das 61 configurações de mão, capturadas pelo sensor Kinect® foi construído. Todas as imagens foram submetidas inicialmente a uma etapa de segmentação que buscou isolar a região da mão direita do resto do corpo. Buscando a eliminação de redundância no conjunto de dados foi implementado uma etapa de extração de características, através da técnica 2D2PCA que determina as formas mais representativas de dados a partir de combinações lineares dos pixels originais. O classificador “k-vizinhos mais próximos” foi a técnica utilizada para a etapa final de reconhecimento automático das configurações de mão. O referido classificador, implementado com k=1 e matriz de característica de 10x10, conseguiu o melhor desempenho, classificando corretamente 96,31% das amostras de testes. Foram obtidas taxas de acerto de 100% para seis configurações de mão.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-01-24T14:59:35Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Aby Akel dos Santos Forte.pdf: 2934639 bytes, checksum: 63baa5bdf64bebdfde01a7e8e4737061 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-01-24T15:00:00Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Aby Akel dos Santos Forte.pdf: 2934639 bytes, checksum: 63baa5bdf64bebdfde01a7e8e4737061 (MD5) / Made available in DSpace on 2018-01-24T15:00:01Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Aby Akel dos Santos Forte.pdf: 2934639 bytes, checksum: 63baa5bdf64bebdfde01a7e8e4737061 (MD5) Previous issue date: 2017-09-12 / The movement for quality and the pursuit of safety in health services is a worldwide phenomenon, due to the growing awareness that, in contemporary society, quality is considered an indispensable requirement of economic survival and, more importantly, according to some authors, a ethical and social responsibility. The hospital maintenance sector, along with the steel / mining sectors, are considered sectors that present the highest cost, of the order of 5 to 10% of the billing in private hospitals. The essential mission of hospital institutions is to serve their patients in the most appropriate way. Therefore, every hospital should be concerned with the permanent improvement of the quality of its management and assistance, seeking a harmonious integration of the medical, technological, administrative, economic, care and, where appropriate, teaching and research areas. The objective of this research was to carry out an improvement plan to be developed at the Heitor Vieira Dourado Tropical Medicine Foundation (FMT_HVD) for the maintenance area in virology management, aiming to improve the activities performed within it, reducing maintenance time of the used machines in this management and change the layout in order to optimize employee time and space within the lab. Lean Manufacturing management tools were used, such as TPM (Total Productive Maintenance) and a database was created with all the operations performed by the management in the virology sector, aiming the monitoring of the useful life of the hospital equipment. After all analyzes in the virology sector and improvements were applied according to Lean Manufacturing methodology, there was a 63% gain in equipment downtime for corrective maintenance due to preventive maintenance. And with regard to the new layout implemented, there was an efficiency gain of 30% with the elimination of wasted time in conducting the tests. The Lean Manufacturing tools proved to be of great value as a way to improve the quality of services performed by increasing productivity and reducing equipment maintenance time, as well as presenting a management philosophy aimed at reducing expenses and waste. / O movimento pela qualidade e busca da segurança nos serviços de saúde é um fenômeno mundial, em decorrência da crescente conscientização de que, na sociedade contemporânea, a qualidade é considerada um requisito indispensável de sobrevivência econômica e, mais importante ainda, segundo alguns autores, uma responsabilidade ética e social. O setor de manutenção hospitalar junto com os setores de siderurgia/mineração são considerados setores que apresentam o custo mais elevado, da ordem de 5% a 10% do faturamento em hospitais particulares. A missão essencial das instituições hospitalares é atender a seus pacientes da forma mais adequada. Por isso, todo hospital deve preocupar-se com a melhoria permanente da qualidade de sua gestão e assistência, buscando uma integração harmônica das áreas médica, tecnológica, administrativa, econômica, assistencial e, se for o caso, de docência e pesquisa. O objetivo desta pesquisa foi realizar um plano de melhoria a ser desenvolvido na Fundação Medicina Tropical Heitor Vieira Dourado (FMT_HVD) para a área de manutenção na gerência de virologia, visando o aprimoramento das atividades exercidas dentro da mesma, reduzindo tempo de manutenção das máquinas utilizadas nesta gerência e alterar o layout a fim de otimizar o tempo dos colaboradores e espaço dentro do laboratório. Foram utilizadas ferramentas de gerenciamento do Lean Manufacturing, como o TPM (Manutenção Produtiva Total) e formado um banco de dados com todas as operações realizadas pela gerência no setor de virologia, visando o acompanhamento da vida útil do equipamento hospitalar. Feitas todas as análises no setor de virologia e aplicadas as melhorias conforme a metodolologia Lean Manufacturing, verificou-se um ganho de 63% no tempo de parada dos equipamentos para a manutenção corretiva devido à manutenção preventiva. E com relação ao novo layout implementado, houve um ganho de eficiência de 30% com a eliminação de tempo desperdiçado na condução da realização de exames. As ferramentas de Manufatura Enxuta mostraram-se de grande valia como forma de aprimorar a qualidade dos serviços realizados, aumentando a produtividade e diminuindo o tempo dos equipamentos em manutenção, além de apresentar uma filosofia de gestão voltada a enxugar despesas e desperdícios.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:38Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:50Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Made available in DSpace on 2018-03-21T17:40:50Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) Previous issue date: 2017-08-10 / FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas / The use of embedded systems, i.e., computer systems focused on performing specific functions in larger (electronic or mechanical) systems, has been growing lately, and ensuring the robustness of such systems has become increasingly important. There are several techniques to ensure that a system is released without errors. In particular, formal verification of programs is proving itself to be effective in the search for failures. In this work, an induction-proof algorithm is described, which combines k-induction and invariants to verify and refute safety properties in embedded ANSI-C software. Moreover, the proposed k-induction-based approach infers invariants in the program to assist in verification tasks, using constraint refinement (i.e., polyhedral) to specify pre- and post-conditions. We adopted two invariant generators to produce such and feed the k-induction algorithm, which is implemented in the Efficient SMT-Based Context-Bounded Model Checker tool. Public benchmarks were used to assess the effectiveness of our approach. In addition, a comparison to other state-of-the-art verification tools using a set of benchmarks from the International Competition for Software Verification in addition to embedded systems applications. Experimental results have shown that the proposed approach, with and without invariants, can verify a wide variety of safety properties in programs with loops and embedded software from telecommunications, control systems, and medical domains. / O uso de sistemas embarcados, sistemas computacionais especializados para execução em sistemas eletrônicos ou mecânicos tem crescido de forma vertiginosa devido a utilização cada vez mais intensa de sensores, interfaces de rede e protocolos de comunicação em diversas áreas. Por isso, é cada vez mais importante garantir a robustez desses sistemas, uma vez que estão se tornando mais complexos e integrados. Existem várias técnicas para garantir que um sistema seja entregue ao cliente sem erros, em particular, a verificação formal dos programas tem se revelado eficaz na busca de falhas. Neste trabalho é descrito um algoritmo de indução matemática conhecido como k-induction combinado ao uso de invariantes para verificar e refutar propriedades de segurança em programas desenvolvidos na linguagem ANSI-C. Em particular, a abordagem proposta infere invariantes no programa para auxiliar na verificação de programas ANSI-C através da técnica de indução matemática através do refinamento de restrição (i.e, poliédrico) para especificar pré- e pós-condições. No método proposto, adotamos dois geradores de invariantes para produzir e alimentar o algoritmo de indução matemática o qual é implementado na ferramenta Efficient SMT-Based Context-Bounded Model Checker. A motivação para a combinação de invariantes com o algoritmo de indução matemática é fechar um gap na verificação formal de programas que possuam variáveis globais, além de programas com loops que possuem desvios condicionais e o número de iterações é desconhecido. PIPS e PAGAI são as ferramentas utilizadas para analisar o código e produzir invariantes indutivas responsáveis por guiar o algoritmo de indução matemática na verificação do benchmark, sendo este o principal desafio do método proposto. Para avaliar a eficácia da abordagem proposta neste trabalho, além de aplicações de Sistemas Embarcados foram utilizados benchmarks públicos disponibilizados pela Competição Internacional de Verificação de Software onde participam Universidades, pesquisadores, estudandantes de doutorado de várias partes do mundo, e fornece amplo conjunto de casos de teste para verificação. Além disso, foram utilizadas ferramentas estado-da-arte para a comparação dos resultados e, assim mensurar a eficácia do método proposto. Os resultados experimentais foram positivos e mostraram que o algoritmo de indução matemática com invariantes pode verificar uma grande variedade de propriedades de segurança em programas com loops e aplicações de sistemas embarcados de telecomunicações, sistemas de controle e dispositivos médicos.