Made available in DSpace on 2016-04-26T20:21:01Z (GMT). No. of bitstreams: 1 Rodrigo Reis Ribeiro Bastos.pdf: 1347780 bytes, checksum: 11f0b6a765aa7c568f8cb75f1cf86311 (MD5) Previous issue date: 2012-06-01 / The primary objective of this work is to understand how they can give concreteness and effectiveness of Article 93 of the Federal Constitution which IX compliance is necessary to guarantee the democratic rule of law. For this to be done there is to discover what are the criteria to be used to identify an adequate justification for decisions. In the first chapter sought to establish the concept of knowledge and the boundary between knowledge and nonsense. At this point it was determined that the root note of knowledge is the rational justification of a statement and that rationality is defined as the construction of a logical proof in the form of inferences. This logical proof must meet three requirements: A) the axiomatic foundations must be explicit; B) the inference rules used must be clearly defined in advance; C) the semantic content (meaning) of the terms used in the premises of proof should be fixed , clarified and explained. Having established that as much knowledge as court decisions have an equal need for justification is concluded that the standards of rational justification used to distinguish the knowledge of the foolish ones are also needed to give concreteness to the constitutional imperative that determines the need to give reasons for decisions . The next step was, in chapter two, establish what the rules of inference commonly used in legal reasoning. Once established the rules of inference has passed the exposure of many reasons most commonly used in decisions. Then, in chapter four, we tried to establish a model where they explained the criteria imposed by law for fixing the best explanation contained in the minor premise and deductions contained in the major premise. Also, if you attempted to make explicit the semantic content (meaning) of the terms that are used on these premises during the construction of algorithms that operate the system. The next step will be, with the use of what has been researched and above, the formulation of "drawing" of the auxiliary system and the creation of a working prototype that can be taken to test / O objetivo primordial desse trabalho é compreender como se pode dar efetividade e concreção ao artigo 93 IX da Constituição Federal cuja observância é necessária para a garantia do Estado Democrático do Direito. Para que isso possa ser feito há que se descobrir quais são os critérios a serem usados para identificar uma adequada fundamentação das decisões. No primeiro capítulo se procurou estabelecer o conceito de conhecimento e a fronteira entre o conhecimento e a tolice. Nesse ponto se estabeleceu que a nota principal do conhecimento é a justificação racional de uma afirmação e que a racionalidade se define como a construção de uma prova lógica na forma de inferências. Essa prova lógica deve atender a três exigências: A) os fundamentos axiomáticos devem estar explícitos; B) as regras de inferência utilizadas devem ser clara e previamente definidas; C) o conteúdo semântico (significado) dos termos usados nas premissas da prova devem ser fixados, esclarecidos e explicitados. Uma vez estabelecido que tanto conhecimento quanto as decisões judiciais possuem uma igual necessidade de justificação se concluiu que os padrões de justificação racional utilizados para diferenciar o conhecimento da tolice também são aqueles necessários para se dar concreção ao imperativo constitucional que determina a necessidade de fundamentação das decisões. O passo seguinte, foi, no capítulo dois, estabelecer quais são as regras de inferência comumente usadas nos raciocínios jurídicos. Uma vez estabelecidas às regras de inferência se passou a exposição dos diversos fundamentos mais comumente usados nas decisões. Em seguida, no capítulo quatro, se tentou estabelecer um modelo onde são explicitados os critérios impostos pelo direito para a fixação da melhor explicação contida na premissa menor e para as deduções contidas na premissa maior. Além disso, se buscou explicitar o conteúdo semântico (significado) dos termos que serão usados nessas premissas quando da construção dos algoritmos que operarão o sistema. O passo seguinte será, com a utilização do que aqui foi pesquisado e exposto, a formulação do desenho do sistema auxiliar e a criação de um protótipo funcional que poderá ser levado a teste

Os sistemas produtivos (SPs) podem utilizar controladores programáveis (CPs) como dispositivos de realização do controle. Neste contexto, programas de controle executados por estes CPs podem ser desenvolvidos de forma que não estejam em conformidade com as especificações de projeto, o que poderá provocar o surgimento de erros funcionais associados à execução de tais programas de controle, erros estes que podem levar os SPs sob controle a um estado que poderá implicar em acidentes envolvendo equipamentos, pessoas e o meio-ambiente. Esta questão tem motivado o surgimento de diversas abordagens para identificar a existência de erros em programas de controle de CPs, de forma a permitir a correção destes erros e garantir, conseqüentemente, maior confiabilidade operacional. O presente trabalho tem por objetivo identificar a existência de erros em programas de controle baseados em LD (Ladder Diagram). Para isto, propõe-se um procedimento de desenvolvimento de modelos baseados em máquinas de estados finitos estendidas (MEFEs), que são gerados a partir do mapeamento de cada um dos rungs contidos no programa de controle que se deseja identificar erros. Uma vez desenvolvidos os modelos em MEFEs, torna-se possível a utilização de uma ferramenta computacional de verificação, própria para estabelecer se os modelos verificados satisfazem determinadas proposições estabelecidas em lógica temporal. Uma proposição em lógica temporal está relacionada a um estado específico do programa de controle modelado, sendo que o objetivo da verificação é o de estabelecer se a proposição estipulada é atendida ou não. Se um determinado estado específico for, por exemplo, um estado indesejado do programa de controle modelado, e este estado for possível de ser alcançado como resultado do processo de verificação realizado, isto impactará na não conformidade do programa de controle com as especificações comportamentais estipuladas na forma de proposição em lógica temporal, indicando haver, portanto, um erro neste programa de controle modelado. Palavras-chave: Controladores programáveis. Linguagem de programação LD. Modelagem e verificação de máquinas de estados finitos estendidas (MEFEs). / Productive systems (PS) can use programmable logic controllers (PLCs) as the devices of accomplishment of the control. In this context, control programs executed by these PLCs can be developed in a way so that they can be in non-conformity with the project specifications, and this fact may result in functional errors related to the control programs execution. These errors can take the PS under control to a state which can lead into accidents involving equipment, people and the environment. This fact has motivated the appearance of different approaches so as to identify the existence of these errors in PLC control programs so that they can be corrected and assure a greater operational reliability. This work aims at identifying the existence of errors in control programs based on Ladder Diagram (LD). In order to accomplish that, a modeling procedure that generates extended finite state machines (EFSMs) is proposed from the mapping of each one of the rungs in the control program whose errors are to be identified. Once the models based on EFSMs are developed it becomes possible to use a computational verification tool, specifically designed to determine if the verified models fulfill determined propositions established in temporal logic. A proposition in temporal logic is related to a specific state of the modeled control program and the objective of the verification is to establish whether the proposition is fulfilled or not. If a determined specific state, for example, is an unwanted state of the modeled control program and if this state is reachable as a result of the verification process, this will impact in the non-conformity of the control program with the behavior specifications established in a temporal logic proposition, indicating an error in this modeled control program.

As análises de erros são conduzidas antes de qualquer projeto a ser desenvolvido. A necessidade do conhecimento do comportamento do erro numérico em malhas estruturadas e não-estruturadas surge com o aumento do uso destas malhas nos métodos de discretização. Desta forma, o objetivo deste trabalho foi criar uma metodologia para analisar os erros de discretização gerados através do truncamento na Série de Taylor, aplicados às equações de Poisson e de Advecção-Difusão estacionárias uni e bidimensionais, utilizando-se o Método de Volumes Finitos em malhas do tipo Voronoi. A escolha dessas equações se dá devido a sua grande utilização em testes de novos modelos matemáticos e função de interpolação. Foram usados os esquemas Central Difference Scheme (CDS) e Upwind Difference Scheme(UDS) nos termos advectivos. Verificou-se a influência do tipo de condição de contorno e a posição do ponto gerador do volume na solução numérica. Os resultados analíticos foram confrontados com resultados experimentais para dois tipos de malhas de Voronoi, uma malha cartesiana e outra triangular comprovando a influência da forma do volume finito na solução numérica obtida. Foi percebido no estudo que a discretização usando o esquema CDS tem erros menores do que a discretização usando o esquema UDS conforme literatura. Também se percebe a diferença nos erros em volumes vizinhos nas malhas triangulares o que faz com que não se tenha uma uniformidade nos gráficos dos erros estudados. Percebeu-se que as malhas cartesianas com nó no centróide do volume tem menor erro de discretização do que malhas triangulares. Mas o uso deste tipo de malha depende da geometria do problema estudado / The analyses of errors are conducted before any project to be developed. The necessity of studying the behavior of the numerical error on structured and unstructured grids comes up with the increasing use of these methods of discretization meshes. Thus, the objective was to create a methodology to analyze the errors generated by discretization of the truncation in the Taylor series, applied to the equations of Poisson and Advection-Diffusion stationary and uni and bi-dimensional, using the Finite Volume Method on Voronoi mesh. The choice of these equations is due to its wide use in testing new mathematical models and interpolation function. The schemes used were the Central Difference Scheme (CDS) and the Upwind Difference Scheme (UDS) in the advective terms. There was the influence of boundary condition and position of the generator in the numerical solution of the volume. The analytical results were compared with experimental results for two types of Voronoi meshes, a Cartesian mesh and a triangular shape showing the influence of finite volume in the numerical solution obtained. It was perceived that the discretization in the study using the CDS scheme has smaller errors than the discretization scheme using the UDS as literature. Also notice the difference in the errors in neighboring volumes in triangular meshes which means that there has been no uniformity in the graphs of errors studied. It was noticed that the Cartesian meshes with node at the centroid of the volume is smaller than discretization error triangular meshes. But using this type of meshes depends on the geometry of the problem studied

A presente tese se refere a três principais objetivos. Um objetivo foi desenvolver um código de simulação numérica direta para simulação de ondas de instabilidade em um escoamento de Poiseuille plano. O outro objetivo foi analisá-Io através do Método das Soluções Manufaturadas (MMS), e por fim, um terceiro objetivo foi estudar o regime não-linear da evolução de trens de ondas modulados em um escoamento de Poiseuille plano. O código resolve numericamente, com diferenças finitas de ordem de precisão alta e métodos pseudo espectrais, as equações de Navier-Stokes tri-dimensionais e incompressíveis numa formulação vorticidade-velocidade. O MMS é um método de verificação de código mais completo que os normalmente usados, por exemplo, comparação com teoria de estabilidade linear. O código usa diferenças finitas de ordem alta de precisão, mas com diferentes ordens em diferentes regiões do domínio. O MMS é pouco utilizado neste tipo de código. Concluiu-se que estes códigos em geral não operam na chamada faixa assintótica de erro. Na faixa de trabalho, a ordem do erro varia no domínio computacional de forma consistente com os métodos numéricos empregados. Isto permite, entre outras coisas, a otimização do esquema numérico. Após os testes de verifição, simulações numéricas dos trens de ondas foram realizadas. A análise dos resultados foi feita através das teorias de instabilidade primária e secundária e teoria fracamente não-linear. Foi estudado um trem de ondas modulado numa região do diagrama de instabilidade onde vários estudos para ondas mono cromáticas foram realizados. Os resultados sugeriram que nesta região o regime não-linear de transição dos trens de ondas modulados é governado pela instabilidade tipo-K. Com a redução da amplitude inicial de perturbação um cenário mais complexo, que pode estar envolvendo outros mecanismos, foi observado. Casos mais próximos ao primeiro ramo do diagrama também foram estudados. Nesta região a teoria linear prevê ondas tri-dimensionais sendo as mais instáveis, fato que poderia favorecer a ocorrência da chamada transição oblíqua. Os resultados indicaram que o trem de ondas modulado se divide em duas regiões que tendem-se afastar uma da outra. Apesar de estar associado com a instabilidade linear, este comportamento não havia sido antecipado na literatura. Neste cenário, para trens de ondas modulados isolados, o regime não-linear não pode ser correlacionado claramente com nenhum dos cenários clássicos de transição. Neste contexto transição oblíqua pode estar restrito a situações que envolvem a interação entre trens de ondas modulados. / The current thesis had three objectives. The first objective was to develop a code of direct numerical simulation (DNS) to simulation of waves of instability in a plane Poiseuille flow. The other main objective was to analyze it through the method of manufactured solutions (MMS). Finally, a third objective was to study the nonlinear regime of spanwise modulated wavetrains in a plane Poiseuille flow. Using high-order finite differences and pseudo-spectral methods, the DNS code solved the incompressible three-dimensional Navier-Stokes equations in a vorticity-velocity formulation. The MMS is a verification method more complete than the others more often used, for example, comparison with linear stability theory. The code used different high-order finite differences in different regions of the domain. The MMS has been little used for this type of code. It was concluded that these codes generally do not operate in the so-called errar asymptotic range. In the working range, the observed arder changes in the computational domain in a manner consistent with the numerical methods employed. This allows, among other things, optimization of the numerical scheme. After testing, numerical simulations of the wavetrains were performed. The analysis of the results was made based on the primary and secondary instability theories and weakly non-linear theory. A modulated wavetrain was studied in a region of the stability diagram where several studies for monochromatic waves were performed. The results suggested that in this region the non-linear regime of transition of the modulation wavetrain is governed by the K-type instability. With the reduction of the magnitude of the initial disturbance, a more complex scenario, which may involve other mechanisms, was observed. Cases near the first branch of the instability diagram were also studied. In this region, the linear theory predicts tri-dimensional waves are the most unstable, a fact that could lead to the so-called oblique transition. The results indicated that the modulated wavetrain divided into two regions, which tend move further from each other. Despite being associated with the linear instability, this behavior was not anticipated in the literature. In this scenario, for isolated modulated wavetrains, the non-linear system could not be clearly correlated with any of the classic scenarios of transition. In this context, oblique transition may perhaps to situations involving the interaction between modulated wavetrains.

O som gerado por escoamentos, também conhecido como aeroacústica, tem se tornado cada vez mais importante em áreas industriais diversas desde aviação comercial até aparelhos eletrodomésticos, afetando diretamente os requisitos necessários para o desenvolvimento de novos produtos. Um caso particular é o ruído gerado por válvulas de compressores herméticos de refrigeração, sendo o compressor a principal fonte de ruído em refrigeradores domésticos. O presente trabalho tem por objetivo iniciar o desenvolvimento de uma ferramenta confiável de simulação capaz de auxiliar engenheiros na predição de problemas de aeroacústica, especialmente um que possa no futuro ser utilizado para estudar o ruído gerado pelo escoamento em válvulas de compressores herméticos. Para isso, foi desenvolvido um código para simulação numérica direta de aeroacústica. Utilizou-se processamento paralelo com decomposição de domínio para usar Simulação Numérica Direta em um tempo factível; esquemas de discretização espaciais e temporais de alta ordem para minimizar ao máximo os fenômenos de dissipação e dispersão do escoamento e das ondas acústicas e uma série de tratamentos no domínio como filtragem e estiramento da malha como também condições de contorno características com o intuito de obter uma solução adequada para estudo de aeroacústica. Assim, são apresentadas todas as etapas desenvolvidas no equacionamento, implementação e verificação. A verificação foi realizada segundo um processo matemático formal (Método das Soluções Manufaturadas) com o qual obteve-se que a ordem de precisão dos cálculos era a mesma da ordem formal dos esquemas de discretização utilizados para todas as variáveis. Também obteve-se a mesma concordância para análise do divergente da velocidade, verificando o código para simulação numérica direta de aeroacústica. Posteriormente, foram realizadas simulações de escoamentos compressíveis cisalhantes e seus resultados comparados com dados apresentados em literatura. Também foram calculadas as taxas de amplificação de perturbações e comparadas com a Teoria de Estabilidade Linear. Novamente, foram obtidos resultados satisfatórios nessas etapas, mostrando que a implementação do código DNS está verificada. / Sound generated by flow, known as aeroacoustics, is becoming more important in several industrial areas from commercial aircraft to household appliances, affecting directly the requirements to the development of new products. A particular case is the noise generated by valves of refrigeration hermetic compressors, being the compressor the main noise source in household refrigerators. This work has the goal of initiate the development of a reliable tool able to help engineers to predict aeroacoustics problems, specially one that can be used in the future to study the noise generated by the flow in valves of hermetic compressors. To do so, it was developed a numerical code to perform direct numerical simulation of aeroacoustics. It was used parallel processing with domain decomposition to use Direct Numerical Simulation in a feasible time; high order temporal and spatial discretization schemes to minimize the most the dispersion and dissipation phenomena of the flow field and of the acoustics waves and a series of treatments in the domain as filtering and mesh stretching as well as characteristics boundary conditions aiming a proper solution to study aeroacoustics. Thus, here all the steps developed in the formulation, implementation and verification are presented . The verification was done according to a formal mathematical procedure (Method of Manufactured Solutions) with which was found that the precision order of the calculations was the same of the formal order of the used discretization schemes for all variables. The same agreement was also obtained to the analysis of the divergence of the velocity, verifying the code to direct numerical simulation of aeroacoustics. Posteriorly, it were simulated shear compressible flows and the results were compared to literature data. Also, it were calculated the amplification rates of the disturbances and compared to Linear Stability Theory. Once more, it was obtained satisfactory results in these steps, showing that the implementation of the DNS code is verified.

O Serviço de Verificação de Óbitos (SVO) foi criado para elucidar causas de óbitos naturais mal definidas por meio de exames necroscópicos e registrar informações mais completas sobre as causas de morte no Sistema de Informação de Mortalidade (SIM). Desde a criação da rede nacional de SVO, poucos estudos avaliaram a qualidade dos registros de óbitos dos SVO no SIM. Foram estudados 19780 registros de óbitos não fetais de residentes no Estado do Tocantins entre os anos de 2012, 2011 e 2012, obtidos por download do site do DATASUS do Ministério da Saúde. Além de estabelecer o perfil social demográfico dos óbitos, foram estudadas a completude das informações, as cinco principais causas de morte e as causas básicas registradas pelo SVO e demais atestantes dentro do SIM. Óbitos do sexo masculino, cor parda, casados, sem escolaridade, hospitalares de aposentados e maiores de 75 anos predominaram. A incompletude de dados registrados no SIM para o Estado do Tocantins foi superior a 10% e não houve diferença estatística significativa entre a completude de dados registrados pelo SVO e pelos demais atestantes. As doenças do aparelho circulatório foram as principais causas de morte registradas pelos atestantes, exceto pelo IML, onde as causas externas predominaram. 15% dos registros de causas básicas externas não pertenciam ao IML e o SVO apresentou uma grande proporção de registros de causas básicas mal definidas. A qualificação das informações sobre mortalidade, imprescindível à elaboração de políticas públicas sanitárias, persiste desafiadora no Estado do Tocantins. A criação de uma cultura da informação epidemiológica passa pela inserção curricular, educação e sensibilização médica continuada. / The Death Verification Service (SVO) was created to elucidate causes of natural deaths poorly defined by postmortem examinations and record more complete information on the causes of death in the Mortality Information System (SIM). Since the establishment of the national network of SVO, few studies have evaluated the quality of death records of SVO SIM. We studied 19780 no fetal death records of residents in the State of Tocantins between the years 2012, 2011 and 2012, downloaded the DATASUS website of the Ministry of Health. In addition to establishing the demographic social profile of the deaths were studied completeness information, the five leading causes of death and root causes recorded by the SVO and other informers within the SIM. Deaths male, mulatto, married, uneducated, retired hospital and over 75 years predominated. The incompleteness of data in SIM for the State of Tocantins was higher than 10% and there was no statistically significant difference between the completeness of data recorded by the SVO and the other informers. The circulatory diseases were the main causes of death recorded by informers except for IML, where external causes predominated. 15% of the records of external root causes did not belong to the IML and the SVO had a large proportion of ill-defined basic causes records. The qualification of information on mortality, essential to the development of health policies, remains defiant in the State of Tocantins. Creating a culture of epidemiological information passes through curriculum integration, education and continuing medical awareness.

As melhores práticas de engenharia de software indicam que a atividade de verificação é fundamental para se alcançar o mínimo de qualidade na construção de um software. Nos processos de desenvolvimento baseados na UML, um dos seus focos principais é detectar inconsistências nos diagramas representativos do software. No entanto, a maioria desses processos, como o Iconix, aplica apenas técnicas informais (ex: inspeções visuais nos modelos), fazendo com que muitas vezes essa atividade seja negligenciada pelos desenvolvedores. Por outro lado, com o avanço das ferramentas automatizadas de verificação, os métodos formais, tais como o Event-B, estão atraindo cada vez mais a atenção das empresas de software. Porém, ainda é difícil convencer os desenvolvedores a adotá-los, pois não estão acostumados com os conceitos matemáticos envolvidos. Assim, este trabalho apresenta uma proposta de inclusão do Event-B no Iconix, dando origem ao BIconix, um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências. Mais especificamente, esta tese aborda a tradução automática dos quatro diagramas existentes no Iconix (classes, casos de uso, robustez e sequência) para o Event-B, além de mostrar como esta formalização pode auxiliar na atividade de verificação em pontos específicos e bem definidos no processo proposto. / The best practices of software engineering indicate that the verification activity is essential to achieve some quality during the software construction. In UML-based development processes, one of its main focuses is the detection of inconsistencies in diagrams that represent the software. However, most of these processes, such as Iconix, apply only informal techniques (eg. visual model inspections), often implying the negligence of that activity by developers. Moreover, with the advance of automated verification tools, formal methods, such as Event-B, are increasingly attracting the attention of software companies. However, it is still difficult to convince developers to adopt them, because they are not acquainted with some mathematical concepts. Thus, this paper presents a proposal for the inclusion of Event-B within Iconix, giving rise to BIconix, an object-oriented development process that supports automatic inconsistencies formal verification. More specifically, this thesis addresses the translation of the four existing diagrams in Iconix (classes, use cases, robustness and sequence) to Event- B, and show how this formalization can assist the verification activity in well-defined check points of the proposed process.

Submitted by Irvana Coutinho (irvana@ufpa.br) on 2015-04-24T13:03:56Z No. of bitstreams: 2 license_rdf: 22974 bytes, checksum: 99c771d9f0b9c46790009b9874d49253 (MD5) Dissertacao_DesenvolvimentoSistemaVerificação.pdf: 7620139 bytes, checksum: 6cf1694753612290ddeead84a3422aba (MD5) / Approved for entry into archive by Ana Rosa Silva (arosa@ufpa.br) on 2015-05-04T11:46:55Z (GMT) No. of bitstreams: 2 license_rdf: 22974 bytes, checksum: 99c771d9f0b9c46790009b9874d49253 (MD5) Dissertacao_DesenvolvimentoSistemaVerificação.pdf: 7620139 bytes, checksum: 6cf1694753612290ddeead84a3422aba (MD5) / Made available in DSpace on 2015-05-04T11:46:55Z (GMT). No. of bitstreams: 2 license_rdf: 22974 bytes, checksum: 99c771d9f0b9c46790009b9874d49253 (MD5) Dissertacao_DesenvolvimentoSistemaVerificação.pdf: 7620139 bytes, checksum: 6cf1694753612290ddeead84a3422aba (MD5) Previous issue date: 2013 / Este trabalho apresenta o desenvolvimento e a aplicação em campo de um sistema para verificação metrológica de transformadores de corrente em alta tensão. O sistema foi desenvolvido utilizando como premissas básicas a portabilidade e a confiabilidade metrológica, de tal forma que pudesse ser facilmente transportado e instalado, sem interrupção do fornecimento de energia elétrica nem o uso de infraestrutura complexa de transporte e montagem. O sistema utiliza como padrão de referência um transdutor ótico, cujo sensor mede a corrente elétrica do primário do transformador de corrente a ser verificado através do efeito magneto-ótico de Faraday. Ele também é composto por outros instrumentos padrão que medem a corrente elétrica do secundário do transformador de corrente sob verificação, e realizam a comparação entre esta e o sinal da saída do transdutor ótico padrão. Foram realizados ensaios em laboratório e em campo. Os ensaios em campo foram realizados em duas subestações em Belém/PA, visando avaliar a correta operação do sistema em condições de alta tensão e alta corrente. Os ensaios foram realizados em seis transformadores de corrente conectados em 230 kV, em condições médias de carga, e obtiveram resultados satisfatórios. / This work presents the development and field application of an on site metrological verification system for high voltage current transformers. It was developed aiming at portability aspects besides the metrological requisites, in such a way it can be easily transported and assembled without the need of power interruption as well as the use of complex and expensive transport and assemble logistics. The system uses an optical transducer as reference standard, whose sensor measures the primary current of current transformer under verification based on Faraday effect It is also composed by additional standard instruments that measure the transformer secondary current under verification, and compares it to the optical transducer output. High voltage laboratory tests as well as on site tests were performed. On site tests were perfomed in two power substations in Brazil, in the city of Belém, in order to assure the correct operation under high voltages and high currents conditions. Six 230 kV rated current transformers were verified. The site tests involved six 230 kV current transformers, under medium load system conditions, and achieved satisfatory results.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2017-08-30T18:56:35Z No. of bitstreams: 1 Avaliacao do uso de coeficientes Mel-cepstrais. MELO, Fabrício Gutemberg L. de..pdf: 4400198 bytes, checksum: b66f2ce2f2e815e517d66cddf8d6be28 (MD5) / Made available in DSpace on 2017-08-30T18:56:35Z (GMT). No. of bitstreams: 1 Avaliacao do uso de coeficientes Mel-cepstrais. MELO, Fabrício Gutemberg L. de..pdf: 4400198 bytes, checksum: b66f2ce2f2e815e517d66cddf8d6be28 (MD5) Previous issue date: 2014-12 / CNPq / A identificação de indivíduos por meio de biometria vem sendo bastante usada como mecanismo de segurança para o acesso a sistemas computacionais ou ambientes restritos. Os sistemas biométricos têm sido desenvolvidos para realizar a identificação por impressão digital, iridia ou vocal, por exemplo. Usar a voz como meio para a autenticação individual tem sido cada vez mais possível, devido ao avanço significativo na área de Processamento Digital de Sinais de voz. Esta pesquisa tem como finalidade avaliar a eficiência dos coeficientes mel-cesptrais na representação das características de um locutor em um sistema automático de verificação de locutor. As técnicas utilizadas para a construção do sistema automático de verificação de locutor, visando a uma implementação em hardware, incluem o uso de: (i) coeficientes mel-cepstrais, na composição do vetor de características; (ii) quantização vetorial, na obtenção de padrões; e (iii) uma regra de decisão, baseada na distância Euclidiana. O sistema utilizado para a avaliação da representação das características vocais de um locutor é uma modificação de outro sistema automático de verificação de locutor que utiliza coeficientes LPC para a representação das características vocais de um locutor. Para tanto, fez-se uso das linguagens C++ (fase de treinamento) e SystemVerilog (fase de verificação). Os resultados utilizando coeficientes mel-cepstrais foram de 99,34% na taxa de acerto, 0,17% para taxa de erros e 0,49% na taxa de respostas desconhecidas, comparados, respectivamente, a 96,52% na taxa de acerto, 0,90% para taxa de erros e 2,58% na taxa de desconhecidos para coeficientes LPC. / Biometric identification of individuals has been widely used as a security mechanism for accessing computer systems or restricted environments. Biometric systems have been developed to perform identification through fingerprint, iris, or voice, for example. Using the voice as a biometric identifier has been increasingly possible due to significant advances in digital processing of speech signals area. This research aims to evaluate the efficiency of mel-frequency cepstral coefficients in the representation of the characteristics of a speaker in an automatic speaker verification. The techniques used to construct the automatic speaker verification system aiming at a hardware implementation included the use of: (i) melfrequency cepstral coefficients, like feature vector; (ii) vector quantization, in patterning modelling; and (iii) a decision rule, based on Euclidean distance. The system used for evaluation in the representation of the characteristics of a speaker is a modification of another automatic speaker verification system using linear predictive coding coefficients for the representation of the vocal characteristics of a speaker. It was implemented using C++ for the training phase, and SystemVerilog for the verification phase. The results using mel-frequency cepstral coefficients were 99.34% in the hit rate, 0.17% to error rate and 0.49% to unknown response rate, compared respectively to 96.52% in success rate, 0.90% to error rate and 2.58% to unknown rate using the linear predictive coding coefficients.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-15T15:44:40Z No. of bitstreams: 1 ANA KARINA DE OLIVEIRA ROCHA - DISSERTAÇÃO PPGCC 2008..pdf: 1111308 bytes, checksum: d22b0170a207a14988449565a953bfb2 (MD5) / Made available in DSpace on 2018-08-15T15:44:40Z (GMT). No. of bitstreams: 1 ANA KARINA DE OLIVEIRA ROCHA - DISSERTAÇÃO PPGCC 2008..pdf: 1111308 bytes, checksum: d22b0170a207a14988449565a953bfb2 (MD5) Previous issue date: 2008-05-16 / A necessidade de sistemas cada vez mais complexos é uma realidade em quase todas as áreas de aplicação da eletrônica. Os avanços recentes da microeletrônica possibilitam o surgimento de soluções inovadoras para diversos problemas do mundo moderno, devido à criação, em ritmo cada vez mais acelerado, de sistemas digitais de qualidade, sendo possível integrar dezenas de milhões de transistores em um único chip, com baixo custo operacional. Esses sistemas estão em constante evolução, impulsionada pelo desenvolvimento da indústria de semicondutores. Assim, há fortes pressões de mercado para a disponibilização de novos produtos com um número cada vez maior de funcionalidades. As implementações dos circuitos eletrônicos complexos necessitam da utilização de metodologias eficientes e automatizadas, que auxiliem na diminuição das falhas de projeto, a exemplo da metodologia de verificação funcional denominada VeriSC, que fornece testbenches e utiliza a biblioteca SCV (SystemC Verification Library), mas se restringe à verificação de circuitos digitais que processam transações temporais síncronas. O trabalho desenvolvido consiste na criação de um mecanismo de implementação de transações temporais, aplicada à metodologia de verificação funcional VeriSC, tornando-a uma metodologia de verificação eficiente também para circuitos digitais capazes de processar transações temporais assíncronas. / The necessity for more complex systems is a reality in almost all electronic application areas. Recent advances in microelectronics make possible the appearance of innovative solutions for several problems of the modern world, due to the creation in accelerated rhythm of quality digital systems, allowing the integration of tens of millions of transistors in a single chip with low operational cost. Those systems are in constant evolution promoted by the development of the semiconductors industry. Thus, there are strong pressures from the market to make new products available with an increasing number of functionalities. Implementations of complex electronic circuits must use of efficient and automated verification methodologies, which help in reducing design failures. In this context VeriSC, a functional verification methodology which provides testbenches and uses the SCV Library (SystemC Verification Library), but it is restricted to the digital circuit verification that has only synchronous time transactions. This work consists in creating a mechanism for the implementation of time transactions, applied to the VeriSC functional verification methodology, and in making it an efficient methodology for digital circuits capable of processing asynchronous time transactions.