Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-06-15T20:18:58Z No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-06-18T19:19:46Z (GMT) No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Made available in DSpace on 2018-06-18T19:19:46Z (GMT). No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) Previous issue date: 2018-02-22 / O uso de Geradores Automáticos de Código para Métodos Formais não apenas minimiza esforços na implementação de Sistemas de Software, como também reduz a chance da existência de erros na execução destes Sistemas. Estas ferramentas, no entanto, podem ter faltas em seus códigos-fonte que causam erros na geração dos Sistemas de Software, e então a verificação de tais ferramentas é encorajada. Esta tese de Doutorado visa criar e desenvolver uma estratégia para verificar JCircus, um Gerador Automático de Código de um amplo sub-conjunto de Circus para Java. O interesse em Circus vem do fato de que ele permite a especificação dos aspectos concorrentes e de estado de um Sistema de maneira direta. A estratégia de verificação consiste nos seguintes passos: (1) extensão da Semântica Operacional de Woodcock e prova de que ela é sólida com respeito à Semântica Denotacional existente de Circus na Teoria Unificada de Programação (UTP), que é um framework que permite prova e unificação entre diferentes teorias; (2) desenvolvimento e implementação de uma estratégia que verifica o refinamento do código gerado por JCircus, através de uma toolchain que engloba um Gerador de Sistema de Transições Rotuladas com Predicado (LPTS) para Circus e um Gerador de Modelos que aceita como entrada (I) o LPTS e (II) o código gerado por JCircus, e gera um modelo em Java Pathfinder que verifica o refinamento do código gerado por JCircus. Através da aplicação do passo (2) combinada com técnicas baseadas em cobertura no código fonte de JCircus, nós visamos aumentar a confiabilidade do código gerado de Circus para Java. / The use of Automatic Code Generators for Formal Methods not only minimizes efforts on the implementation of Software Systems, but also reduces the chance of existing errors on the execution of such Systems. These tools, however, can themselves have faults on their source codes that may cause errors on the generation of Software Systems, and thus verification of such tools is encouraged. This PhD thesis aims at creating and developing a strategy to verify the code generation from the Circus formal method to Java Code. The interest in Circus comes from the fact that it allows the specification of concurrent and state-rich aspects of a System in a straightforward manner. The code generation envisaged to be verified is performed by JCircus, a tool that translates a large subset of Circus to Java code that implements the JCSP API. The strategy of verification consists on the following steps: (1) extension of Woodcock’s Operational Semantics to Circus processes and proof that it is sound with respect to the Denotational Semantics of Circus in the Unifying Theories of Programming (UTP), that is a framework that allows proof and unification of different theories; (2) development and implementation of a strategy that refinement-checks the code generated by JCircus, through a toolchain that encompasses (2.1) a Labelled Predicate Transition System (LPTS) Generator for Circus and (2.2) a Model Generator that inputs (I) a LPTS and (II) the code generated by JCircus, and generates a model (that uses the Java Pathfinder code model-checker) that refinement-checks the code generated by JCircus. Combined with coverage-based techniques on the source code of JCircus, we envisage improving the reliability of the Code Generation from Circus to Java.

Made available in DSpace on 2015-05-14T12:09:37Z (GMT). No. of bitstreams: 1 arquivototal.pdf: 10447871 bytes, checksum: f75e368c81366ea6407b5bdfc036035e (MD5) Previous issue date: 2014-09-22 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / Precipitation is a weather element that serves as the key to most types of analysis input parameter. However, traditional systems of collecting budget record historical, geographical and temporal in obtaining, processing and transfer problems. This fact has mobilized the rise of techniques such as orbital remote sensing (ORS), increasingly applied in studies aimed at monitoring and forecasting through Hydrological Models such as the Distributed Hydrological Models (DHM). However, because they are considered the ground truth science requires intercomparison of results from orbital sensors with them in order to have the analytical scrutiny of verification of responses from performance. However, the methodologies adopted in the comparative analysis of their results - with terrestrial information - usually do not report the nature of the error information, if basing only on larger or smaller link the information. Therefore, this paper aims to contribute to science through the methodological increase with use of statistics related to performance indicators, to assess the particularities involved in the errors associated with each sensor element for measuring rain. Methodologically compared the information of rain sensor 3B42 algorithm s 7 version of Tropical Rainfall Measurement Mission (TRMM) with historical information from rain gauges belonging to Agência Executiva de Gestão de Águas do Estado da Paraíba (AESA), with analysis from 1998 to the year 2011, were methodologically compared followed two analytical biases. At first, there was the spatio-temporal similarity to pixel level (pixel-to-pixel) in what is called approach 1 (A1); and second, there was the similarity of the results in quantitative precipitation bands. Results in analytical approach 1 (A1), the TRMM showed good performance on measures of agreement for negative events correct. According to the second approach (A2) the performances presented to corroborate the depreciation of the estimated sensor. / A precipitação é um elemento meteorológico que serve como parâmetro de entrada fundamental aos mais diversos tipos de análise. No entanto, os sistemas tradicionais de coleta registram históricos problemas orçamentais, geográficos e temporais na sua obtenção, processamento e repasse. Tal fato tem mobilizado a ascensão de técnicas, como o sensoriamento remoto orbital (SRO), que cada vez mais se aplica nos estudos voltados ao monitoramento e previsão, em conjunto com os Modelos Hidrológicos, tal como os Modelos Hidrológicos Distribuídos (MHD). No entanto, por serem considerados a verdade de campo a ciência exige a intercomparação dos resultados dos sensores orbitais com os mesmos afim de se ter o crivo analítico da verificação de respostas de desempenho. Entretanto, as metodologias adotadas na análise comparativa dos seus resultados - com as informações terrestres - normalmente não informam a natureza dos erros de informação, pautando-se apenas na relação maior ou menor entre as informações. Portanto, o trabalho objetiva contribuir com a ciência, por meio de proposta metodológica, com uso de estatísticas ligadas a índices de desempenho, de forma a avaliar as particularidades envolvidas nos erros associados entre sensores de mensuração do elemento chuva no estado da Paraíba. Metodologicamente comparou-se as informações de chuva do algoritmo 3B42 da Versão 7, do sensor orbital Tropical Rainfall Measurement Mission (TRMM) com as informações históricas dos postos pluviométricos pertencentes a Agência Executiva de Gestão de Águas do Estado da Paraíba (AESA), entre os anos de 1998 a 2011. Seguiu-se dois vieses analíticos. No primeiro momento, verificou-se à similaridade espaço-temporal ao nível do pixel (pixel-a-pixel) no que se denomina primeira abordagem (A1); e no segundo, verificou-se à similaridade dos resultados sob faixas quantitativas de chuva, no que se nomeia segunda abordagem (A2). Como resultados na abordagem analítica A1, o TRMM apresentou bons desempenhos às medidas de concordância para eventos de correto negativos. Segundo a abordagem A2 os desempenhos apresentados corroboraram para maiores erros da estimativa do sensor.

Submitted by Ivan Oliveira Lopes (io.lopes@ifsp.edu.br) on 2018-09-22T02:34:15Z No. of bitstreams: 1 MARDI_Marca dagua Robusta via Decomposicao de Imagens.pdf: 69551246 bytes, checksum: 895274cb196d7f5075a7bf92bba60e9f (MD5) / Approved for entry into archive by Cristina Alexandra de Godoy null (cristina@adm.feis.unesp.br) on 2018-09-25T19:59:12Z (GMT) No. of bitstreams: 1 lopes_io_dr_ilha.pdf: 69617454 bytes, checksum: 7a93538756770bc0935aa4b85b95f4b7 (MD5) / Made available in DSpace on 2018-09-25T19:59:12Z (GMT). No. of bitstreams: 1 lopes_io_dr_ilha.pdf: 69617454 bytes, checksum: 7a93538756770bc0935aa4b85b95f4b7 (MD5) Previous issue date: 2018-07-27 / Com a crescente evolução dos equipamentos eletrônicos, muitos dados digitais têm sido produzidos, copiados e distribuídos com facilidade, gerando uma grande preocupação com a sua segurança. Dentre as várias técnicas usadas para proteger os dados digitais, tem-se as técnicas de inserção e extração de marca d'água em imagens digitais. Uma marca d'água pode ser qualquer informação como, por exemplo, um código, um logotipo, ou uma sequência aleatória de letras e números, que vise garantir a autenticidade e a proteção dos direitos autoriais dos dados. Neste trabalho, estudou-se sobre as técnicas existentes de inserção e extração de marca d'água digital, abordando desde seu conceito até o desenvolvimento de algoritmos de inserção e extração de marca d'água em imagens digitais. Desenvolveu-se um método para aumentar a robustez de técnicas de marca d' água digital pela decomposição da imagem em duas partes: estrutural (áreas homogêneas) e de detalhes (áreas com ruídos, texturas e bordas). Contudo, a marca d'água é inserida na parte de detalhes por se tratar de áreas menos afetadas por operações de processamento digital de imagens. Os resultados mostraram que o método proposto aumentou a robustez das técnicas da marca d'água testadas. Baseado nos resultados obtidos, desenvolveu-se uma nova técnica de marca d'água digital, utilizando a transformada discreta de wavelets, a decomposição de imagens e a transformada discreta do cosseno. / With the increasing evolution of technological equipment, many digital data have been easily produced, copied and distributed by generating a great concern for their security. Among the various techniques used to protect the digital data, there are techniques for inserting and extracting a watermark into digital images. A watermark can be any information, such as a code, a logo, or a random sequence of letters and numbers, aiming to ensure the authenticity and copyright protection. In this work are studied, existing insertion and extraction techniques in digital watermarking, by covering from its concept to the development of watermark insertion and extraction algorithms, in digital images. A method was developed to increase the robustness of digital watermarking techniques by decomposing the image into two parts: structural (homogeneous areas) and details (areas with noises, textures and edges). However, the watermark is inserted in the detail area due to be less affected areas by digital image processing. The results showed that the proposed method increased the robustness of the tested watermarking techniques. Based on the results obtained, we developed a new digital watermark technique using discrete wavelet transform, image decomposition and discrete cosine transform.

O desenvolvimento de sistemas críticos é atualmente um dos problemas mais desafiadores enfrentados pela Engenharia. Há frequentemente uma pressão para se reduzir o tempo total de desenvolvimento, o que dificulta a entrega de sistemas com um mínimo aceitável de defeitos. Nos últimos anos, houve um aumento no tráfego aéreo, o que demanda uma modernização dos sistemas de tráfego aéreo atuais, muito dependentes na figura do controlador. Sistemas de tráfego aéreo são sistemas considerados críticos em segurança e de tempo real. O objetivo do presente trabalho é estabelecer um método de modelagem e verificação formal para sistemas críticos, com aplicação no domínio de tráfego aéreo. Com a adoção de técnicas de modelagem e verificação formal, pretende-se garantir a corretude dos sistemas frente aos requisitos inicialmente especificados e a detecção de erros em fases mais iniciais do projeto, o que resultaria em menores custos envolvidos na sua correção. São fornecidas diretivas para a aplicação do método através de um estudo de caso, baseado em três módulos de um sistema ATC em baixo nível de abstração, para a validação do funcionamento de módulos de software. Para verificação formal, é utilizada a ferramenta NuSMV e as propriedades a serem verificadas são descritas na lógica computacional de árvore (CTL) para garantir que o sistema satisfaça requisitos dos tipos vivacidade e segurança. / Developing safety critical systems is one of the most challenging problems in Engineering nowadays. There is usually a pressure to reduce the total time of the development, what makes it difficult to deliver systems with an acceptable low level of defects. In the recent years, there has been an increase in air trffic, what demands a modernization in the current air traffic systems, which are very dependent on the human controller. Air traffic systems are considered safety critical and real time systems. The objective of the present work is to establish a modeling and formal verification method for critical systems, applicable to the air traffic domain. By adopting modeling and formal verification techniques, it is expected to ensure the systems\' correctness compared with the initially specified requirements and the error detection in the initial phases of the project. Guidelines are provided for applying the method by means of a case study, based in three modules of and ATC system in a low abstraction level, for the validation of the operation of software modules. For the formal verification, it is used the NuSMV tool and the properties to be checked are described in the computational tree logic (CTL) to ensure that the system satisfies requirements of liveness and safety types.

Devido à alta complexidade dos Sistemas Produtivos, o projeto de sistemas de controle adequados às exigências normativas vinculadas aos processos industriais que são executados, e seu impacto no ser humano e no ambiente demandam a necessidade do desenvolvimento de soluções de controle que sejam seguras e estáveis no sentido de não causar interrupções no processo produtivo e danos ao ser humano e ao meio. Uma abordagem para o desenvolvimento de sistemas que contemplem estes requisitos baseia-se no conceito de Sistemas Instrumentados de Segurança e na aplicação das normas IEC 61508 e IEC 61511. Entretanto, assim como o desenvolvimento de qualquer software, os programas de controle de SIS também estão sujeitos a erros de especificação e projeto, mesmo quando o desenvolvimento é feito conforme os critérios normatizados. Além dos erros de projeto, também deve ser levado em consideração que as camadas de prevenção e mitigação especificadas nas normas podem ser desenvolvidas separadamente e dessa forma podem ocorrer comportamentos não previstos ou indesejáveis quando da operação conjunta delas. Uma das formas para uma melhoria na confiabilidade desses programas e que também é um requerimento pertinente ao ciclo de desenvolvimento de um SIS - de acordo com as normas de segurança IEC 61508 e IEC 61511 - é a aplicação de técnicas de verificação formal dos modelos desses programas de controle bem como o uso de um ambiente unificado para modelagem desses sistemas de controle, onde suas interações possam ser mais bem compreendidas. Atualmente, umas das técnicas mais proeminentes para a verificação de sistemas é o Model Checking, que realiza uma busca exaustiva no espaço de estados de um sistema dirigido por eventos, verificando as propriedades especificadas a partir de proposições estabelecidas em lógica temporal. Para esse trabalho é utilizada a lógica TCTL devido a sua capacidade de expressar propriedades em domínio temporal denso. Como ferramenta computacional será usado o ambiente GHENeSys, que propicia um ambiente unificado para modelagem, simulação e verificação dos sistemas por conjugar os benefícios de rede de Petri para modelagem e as técnicas de Model Checking para verificação de modelos. / Due to the high complexity of the actual Productive Systems, the design of suitable control systems according to the applicable industrial standards, and the possible negative impacts on the human being, on the environment and on equipment, the development of control solutions that are be both secure and stable as some systems have to operate nonstop is much demanded. One approach for the development systems with such requirements is the use of Safety Instrumented Systems complying with the standards IEC 61508 and IEC 61511. However, as on the development of any kind of software, SIS control programs are also prone to specification and design errors, even when the control programs are developed according to the applicable standards. Besides design errors, must be taken into consideration the fact that the SIS prevention and mitigation layers, as prescribed on the standards, can be developed individually and thus presenting unanticipated or undesirable behaviors when operating together. One way to improve the reliability of these control programs, which is also required by the safety standards IEC 61508 and IEC 61511 as part of the SIS development cycle, is the application of formal verification techniques on the control software models. Another way is to use a unified approach for modeling these control systems, and thus having the opportunity to understand their interactions better. Currently, one of the most prominent techniques for the verification of systems is the Model Checking. Such technique performs an exhaustive search in the space state of an event driven system, verifying the properties specified as established propositions in temporal logic. On this work, the TCTL logic is used due its ability to express properties in the dense time domain. As computational tool will be used GHENeSys environment, as it provides a unified environment for modeling, simulating and the verification of systems, which enjoys the benefits of modelling through Petri Nets and Model Checking techniques for formal verification.

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2016-06-13T13:50:41Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Dissertação - Davi Delgado Clerot - UFPE.pdf: 1275511 bytes, checksum: 8413259c0fde19c85569221d062625a8 (MD5) / Made available in DSpace on 2016-06-13T13:50:41Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Dissertação - Davi Delgado Clerot - UFPE.pdf: 1275511 bytes, checksum: 8413259c0fde19c85569221d062625a8 (MD5) Previous issue date: 2014-04-28 / No âmbito da biometria comportamental, o reconhecimento automático de assinaturas manuscritas off-line se destaca pela boa aceitação em diversos segmentos, tais como Bancos, Cartórios e Imobiliárias. Dentre os fatores que estimulam sua utilização estão a facilidade na aquisição, pois não depende de equipamentos específicos, e seu valor legal ao ser realizada de próprio punho. No intuito de investigar métodos alternativos para realizar sua verificação automática, esta dissertação testa uma abordagem baseada no Coeficiente de Correlação de Pearson. O experimento foi realizado em seis etapas; da primeira à terceira, são utilizadas variações na extração de características, sem o auxílio de um classificador baseado em aprendizado automático. No quarto experimento, foi utilizada uma rede neural artificial como classificador, para efeito de comparação com os resultados anteriores. No quinto experimento, um peso associado ao limiar de resposta utilizado nos experimentos anteriores foi adicionado objetivando minimizar efeitos dos falsos positivos obtidos. No sexto e último experimento, para efeito de comparação com trabalhos relacionados, foi utilizada a base de dados disponibilizada no ICDAR (Conferência Internacional em Reconhecimento e Análise de Documentos) 2011. A configuração empregada nesta etapa, a qual utilizou a base do ICDAR, foi a do melhor experimento realizado dentre os anteriores. Os métodos propostos apresentaram resultados promissores em comparação com os resultados apresentados na literatura. / In the field of behavioral biometrics, automatic off-line handwritten signature recognition stands out for its widespread acceptance in different market segments, such as Banks, Civil Registry Offices and Real State Agencies. Among the reasons why its use is widely stimulated are its ease of acquisition, once it does not depend on specific equipment, and its legal value when it is done by the author’s own handwriting. With the purpose of searching for alternative methods to proceed to its automatic verification, this essay tests out an approach based on Pearson Correlation Coefficient. The experiment was carried out through six steps; from the first to the third ones, there were used variations for feature extraction, without the assistance of a learning classifier. In the fourth experiment, there was used an artificial neural network as a classifier, in order to compare its results with those obtained in the previous tests. In the fifth experiment, a weight associated to the threshold results obtained in the previous experiments was added, so as to minimize the false positive rate. In the sixth and last experiment, for comparison with related essays, there was used the ICDAR (International Conference on Document Analysis and Recognition) 2011 database. The configuration utilized in this last step was the one obtained in the best test among the previous ones. The proposed methods presented promising results compared to others reported in the literature.

Submitted by Geyciane Santos (geyciane_thamires@hotmail.com) on 2015-07-23T13:51:53Z No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:49:26Z (GMT) No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:52:49Z (GMT) No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) / Made available in DSpace on 2015-07-23T15:52:49Z (GMT). No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) Previous issue date: 2013-12-20 / FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas / The use of embedded systems, computational systems specialized to do a function in larger systems, electronic or mechanical, is growing in the daily life, and it is becoming increasingly important to ensure the robustness of these systems. There are several techniques to ensure that a system is released without error. In particular, formal verification is proving very effective in finding bugs in programs. In this work, we describe the formal verification for C++ Programs and correctness proof by mathematical induction. Both techniques will be developed using the tool Efficient SMT-Based Context-Bounded Model Checker (ESBMC), a model checker based on satisfiability modulo theories and first order logic. The experiments show that the tool can be used to check a wide range of applications, from simple test cases to commercial applications. The tool also proved to be more efficient than other models checkers to verify C++ programs, finding a greater number of bugs, and supporting a larger number of the features that the language C++ has to offer, in addition to being able to prove several properties, using the method of mathematical induction. / A utilização de sistemas embarcados, sistemas computacionais especializados para realizar uma função em sistemas maiores, eletrônicos ou mecânicos, vem crescendo no dia a dia das pessoas, e vem se tornando cada vez mais importante garantir a robustez desses sistemas. Existem diversas técnicas para garantir que um sistema seja lançado sem erros. Em especial, a verificação formal de programas está se mostrando efetiva na busca por falhas. Neste trabalho, serão descritos a verificação formal de programas C++ e a prova de corretude por indução matemática. Ambas as técnicas serão desenvolvidas utilizando a ferramenta Efficient SMTBased Context-Bounded Model Checker (ESBMC), um verificador de modelos que se baseia em teorias de satisfabilidade de fórmulas proposicionais e de lógica de primeira ordem. Os experimentos mostram que a ferramenta pode ser utilizada para verificar uma ampla gama de aplicações, de casos simples à aplicações comerciais. A ferramenta também mostrou-se superior em comparação com outros verificadores na verificação de programas C++, encontrando um maior número de erros e suportando um número superior das funcionalidades que a linguagem C++ tem a oferecer, além de ser capaz de provar diversas propriedades (por exemplo, laços invariantes), utilizando a técnica de indução matemática.

Submitted by Kamila Costa (kamilavasconceloscosta@gmail.com) on 2015-08-03T12:38:15Z No. of bitstreams: 2 Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5) ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-08-04T15:34:24Z (GMT) No. of bitstreams: 2 Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5) ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-08-04T15:38:25Z (GMT) No. of bitstreams: 2 Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5) ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) / Made available in DSpace on 2015-08-04T15:38:25Z (GMT). No. of bitstreams: 2 Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5) ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) Previous issue date: 2015-04-01 / CNPq - Conselho Nacional de Desenvolvimento Científico e Tecnológico / The development of programs written in Lua programming language, which is largely used in applications for digital TV and games, can cause errors, deadlocks, arithmetic overflow, and division by zero. This work aims to propose a methodology for checking programs written in Lua programming language using the Efficient SMT-Based Context-BoundedModel Checker (ESBMC) tool, which represents the state-of-the-art context-bounded model checker. It is used for ANSI-C/C++ programs and has the ability to verify array out-of-bounds, division by zero, and user-defined assertions. The proposed approach consists in translating programs written in Lua to an intermediate language, which are further verified by ESBMC. The translator is developed with the ANTLR (ANother Tool for Language Recognition) tool, which is used for developing the lexer and parser, based on the Lua language grammar. This work is motivated by the need for extending the benefits of bounded model checking, based on satisfiability modulotheories, to programs written in Lua programming language. The experimental results show that the proposed methodology can be very effective, regarding model checking (safety) of Luaprogramming language properties. / O desenvolvimento de programas escritos na linguagem de programação Lua, que é muito utilizada em aplicações para TV digital e jogos, pode gerar erros, deadlocks, estouro aritmético e divisão por zero. Este trabalho tem como objetivo propor uma metodologia de verificação para programas escritos na linguagem de programação Lua usando a ferramenta Efficient SMT-Based Context-Bounded Model Checker (ESBMC), que representa o estado da arte em verificação de modelos de contexto limitado. O ESBMC é aplicado a programas embarcados ANSI-C/C++ e possui a capacidade de verificar estouro de limites de vetores, divisão por zero e assertivas definidas pelo usuário. A abordagem proposta consiste na tradução de programas escritos em Lua para uma linguagem intermediária, que é posteriormente verificada pelo ESBMC. O tradutor foi desenvolvido com a ferramenta ANTLR (do inglês “ANother Tool for Language Recognition”), que é utilizada na construção de analisadores léxicos e sintáticos, a partir da gramática da linguagem Lua. Este trabalho é motivado pela necessidade de se estender os benefícios da verificação de modelos, baseada nas teorias de satisfatibilidade, a programas escritos na linguagem de programação Lua. Os resultados experimentais mostram que a metodologia proposta pode ser muito eficaz, no que diz respeito à verificação de propriedades (segurança) da linguagem de programação Lua.

A poluição sonora é um problema central de uma grande diversidade de aplicações industriais. Na engenharia, podemos citar diversos casos que geram ruído, como exemplos os trens, automóveis, rotores de helicópteros e o ruído aerodinâmico das aeronaves, o qual se divide em ruído gerado pelos motores a jato e a estruturas da aeronave. No presente momento o ruído dos motores aeronáuticos, principalmente os jatos, atingiu níveis de ruídos semelhantes às estruturas da aeronave, como por exemplo, eslates, flaps e trens de pouso. Desta forma, as autoridades de transporte aéreo estão exigindo também redução no ruído das estruturas. O presente trabalho apresenta a verificação das potencialidades e limitações do software CFD++, programa este adquirido pela EMBRAER e inserido como parte do projeto Aeronave Silenciosa, para assim poder compreender de uma melhor maneira o fenômeno da aeroacústica, e deste modo, poder contribuir para a redução do ruído externo das aeronaves. Para verificar as potencialidades e limitações do CFD++, foi proposto investigar o mecanismo de som do eslate. Tal fenômeno é devido ao deslocamento da camada limite no intradorso do eslate a partir de onde se desenvolve a camada de mistura, foco do presente trabalho. / Noise pollution is a central problem of a wide variety of industrial applications. In engineering, cite several cases that generate noise, as examples trains, automobiles, rotors of helicopters and the noise generated by aircraft, which is divided into noise generated by jet engines and airframe. At present the noise of aircraft engines, largely the jets reached noise levels similar structures, such as slat, flaps and landing gear. Thus, the air transport authorities are also demanding a reduction in noise of the structures of airframe. This report presents the verification of potentialities and limitations of CFD++, a program acquired by EMBRAER and inserted as part of the Silent Aircraft, so they can understand better how the phenomenon of aeroacoustics, and thus able to reduce contribute external noise from aircraft. To check the potentialities and limitations of CFD++, was proposed to investigate the mechanism of sound generated by the slat. This phenomenon is due to the displacement of the boundary layer on the lower surface of the slat from which the mixed layer develops. The mixing layer is the focus of this work.

Este estudo tem como objetivo a verificação das previsões diárias, das temperaturas máxima e mínima e precipitação acumulada, realizadas pelo modelo operacional de previsão numérica do tempo WRF (Weather Research Forecasting) para o estado de São Paulo. As condições iniciais e de fronteira fornecidas pela análise e previsão das 00UTC do modelo Global Forecast System (GFS), são usados no processamento do WRF, para previsões de 72 horas, em duas grades aninhadas (espaçamentos horizontais de grade de 50 km, D1, e 16,6 km, D2). O período avaliado foi de abril de 2010 a março de 2011. As comparações diárias das temperaturas máxima e mínima foram realizadas entre os valores preditos e observados nas estações de superfície de Registro, São Paulo, Paranapanema, Campinas, Presidente Prudente e Votuporanga (dados da CIIAGRO); através do erro médio (EM) e raiz do erro médio quadrático (REQM), para os prognósticos das 36, 60 e 72 horas. A precipitação acumulada diária é avaliada com relação ao produto MERGE, pela aplicação da ferramenta MODE, na previsão das 36 horas, para um limiar de 0,3 mm, no domínio espacial abrangendo o Estado de São Paulo e vizinhanças. Primeiramente, fez-se uma análise, comparando os pares de grade dos campos previsto e observado, utilizando os índices estatísticos de verificação tradicional de probabilidade de acerto (PA); índice crítico de sucesso (ICS); viés (VIÉS); probabilidade de detecção (PD) e razão de falso alarme (RFA). Posteriormente, foram analisados os campos de precipitação com relação à razão de área (RA); distância dos centroides (DC); razões de percentil 50 (RP50) e 90 (RP90). Os resultados evidenciaram que as saídas numéricas do modelo WRF com D2 tiveram desempenho melhor comparado à grade de menor resolução (maior espaçamento de grade horizontal, D1), tanto no prognóstico diário das temperaturas (máxima e mínima) quanto da precipitação acumulada. A temperatura apresentou um padrão de amortecimento, com temperaturas diárias máxima subestimada e mínima superestimada. Com relação à precipitação, as saídas numéricas do modelo GFS e WRF com D2 mostraram desempenho semelhante, com o D2 apresentando índices ligeiramente melhores, enquanto que as saídas numéricas do modelo WRF com D1 exibiram pior desempenho. Verificou-se um padrão de superestimativa, tanto em termos de abrangência espacial quanto em intensidade, para o modelo GFS e WRF em ambos os domínios simulados, ao longo de todo o período analisado. O percentil 50 é, geralmente, maior que o observado; entretanto, o percentil 90 é mais próximo ao observado. Os resultados também indicam que o viés dos modelos varia ao longo do ano analisado. Os melhores índices tanto com relação à precipitação quanto à temperatura foram obtidos para a estação de verão, com o modelo WRF com D2 apresentando melhores prognósticos. Entretanto, os modelos apresentam os maiores erros no inverno e no outono. Estes erros foram decorrentes de subestimativas das temperaturas máximas e superestimativas de área e intensidade de precipitação. / Forecasts of daily maximum and minimum temperatures and rainfall performed by the operational numerical weather prediction WRF (Weather Research Forecasting) model in the São Paulo are evaluated. Initial and boundary conditions provided by the 00UTC Global Forecast System (GFS) Model and WRF run for 72 hours, with two nested grids (with horizontal grid spacing of 50 km, D1, and 16.6 km, D2). The study was made for April 2010 to March 2011 period. Daily maximum and minimum temperatures comparisons were made, between predicted and observed data of the surface weather stations of Registro, São Paulo, Paranapanema, Campinas, Presidente Prudente and Votuporanga (CIIAGRO Data), through the mean error (ME) and root mean square error(RMSE), for the 36, 60 and 72 hours forecasts. The daily accumulated rainfall is evaluated using MODE with respect to the MERGE product, for the 36 hours forecast, with threshold of 0.3 mm over the spatial domain covering the State of São Paulo and neighborhoods. First, an analysis was made comparing grid pairs of predicted and observed fields, through the traditional statistical verification indexes: accuracy (PA), critical success index (ICS), bias (VIES), probability of detection (PD) and false alarm ratio (RFA). Subsequently, we analyzed the precipitation field with respect to area ratio (AR), distance from the centroids (DC), ratio of the 50th percentile (RP50) and ratio of the 90th percentile (RP90). The WRF, with D2 nested grid, had better performance compared to the grid of lower space resolution (higher horizontal grid spacing, D1) for both, daily temperatures (maximum and minimum) and the accumulated rainfall forecasts. The temperature forecast presented a damped pattern, with underestimated maximum and overestimated minimum values. Rainfall was overall overestimated spatially and in intensity for the three models throughout the analized period. The forecasted 50th percentile is generally higher than that observed, however, the 90th percentile is closer to observations. The results also indicate that the bias of the models varies annually. The best performances for both rainfall and temperature were obtained for the summer season, with the D2 showing slightly better results. However, the models had the biggest errors during the winter and autumn seasons. These errors were due to underestimation of maximum temperatures and overestimation in area and intensity of precipitation.