Neste trabalho apresentamos uma implementação de revisão de crenças baseada em comparação de modelos (estados) em uma ferramenta de verificação automática de sistemas de estados finitos. Dada uma fórmula (na lógica CTL) inconsistente com o modelo do sistema, revisamos esse modelo de tal maneira que essa fórmula temporal se torne verdadeira. Como temos oito operadores temporais (AG, AF, AX, AU, EG, EF, EX e EU), foram criados algoritmos especícos para cada um deles. Como o modelo do sistema deriva do seu código na linguagem SMV, a sua revisão passa obrigatoriamente por mudanças na sua descrição. A nossa implementação contempla três tipos de mudanças: acréscimo de linhas, eliminação de linhas e mudança no estado inicial, sendo que as duas primeiras provocam modicações nas transições entre os estados que compõe o modelo. Alguns testes foram aplicados para comprovar a contribuição da revisão de crenças (revisão de modelos) como ferramenta de auxílio ao usuário durante o processo de modelagem de sistemas. / In this work we present an implementation of belief revision based on comparison of models (states) in a tool for automatic verication of nite state systems. Given a formula (in the language of CTL) inconsistent with the model of the system, we revise this model in such way that the temporal formula becomes valid. As we have eight temporal operators (AG, AF, AX, AU, EG, EF, EX and EU), specic algorithms for each one of them have been created. As the model of the system is related with its code in SMV language, its revision forces changes in its description. Our implementation contemplates three types of change: addition of lines, elimination of lines and change in the initial state, where the rst two cause modications in the transitions between the states of the model. Some tests were applied to prove the contribution of the belief revision (model revision) as aid-tool to the user during the process of systems modeling.

Um sistema de software que apresente problemas em sua execução pode gerar conseqüências desde um simples incômodo ao usuário, até desastres como a perda de uma sonda da NASA em Marte. As atividades de teste visam identificar erros nos sistemas de software, prevenindo estas conseqüências indesejáveis. Porém, os testes podem envolver entre 30% e 40% do esforço de desenvolvimento do sistema, e em sistemas críticos, seu custo pode ser de 3 a 5 vezes maior do que o custo combinado das demais atividades. Para tentar reduzir estes custos podemos automatizar parte das atividades. No presente caso, pretende-se minimizar os casos de teste gerados manualmente, utilizando uma técnica denominada verificação de modelos. Esta técnica consiste em verificar propriedades definidas formalmente através de expressões matemáticas, utilizando uma ferramenta de verificação que simula a execução do código. Além disso, um sistema que utilize um tratamento de condições excepcionais eficiente, tem sua manutenibilidade, robustez e confiabilidade melhoradas. Por isso, definimos propriedades relacionadas ao tratamento de exceções, como ponto de entrada para a verificação de modelos. Apresentamos um ambiente de testes criado para permitir a verificação destas propriedades com o verificador Java PathFinder e a exibição das estatísticas de cobertura de testes de acordo com o critério selecionado. Este ambiente facilita a execução dos testes, pois apresenta uma interface gráfica com o usuário que permite a configuração e execução dos testes sem que seja necessária a escrita de código pelo testador. Apresentamos também o resultado do uso deste ambiente para o teste de vários programas exemplo, utilizando desde código concorrente até diferentes estratégias de tratamento de exceção e discutimos as características, cuidados no uso e limitações das ferramentas utilizadas. / A software system that shows some failure at runtime execution may bring consequences that range from a simple user annoyance to great disasters such as the lost NASA probe on Mars. The test activities aim to find errors in software systems, preventing these undesirable consequences. However, tests may take between 30% and 40% of total development time, and on critical systems, its cost can be from 3 to 5 times greater than the combined cost of the other activities. In an effort to reduce these costs, we may automate some of the activities. In this work we intend to minimize test case manual generation, using a technique called model checking. This technique involves the checking of properties defined through the use of mathematical formulas, using a tool, that simulates code execution. In addition, a system with an efficient exception handling mechanism, has its maintainability, robustness and reliability enhanced. So, in this work we define exception handling related properties, as an input for model checking. We present a test tool created to allow checking of these properties using the Java PathFinder model checker, and to list the test coverage statistics, according to the selected test criteria. This tool makes easy the test execution, since it presents a graphical user interface that allows configuration and running of tests with no need to write any lines of code. We also show the results of running several tests with the GUI, using some programs implemented with concurrent code and several exception handling techniques and discuss the main features, pitfalls and limitations of the underlying tools.

Verificação de modelos é uma das mais eficientes técnicas de verificação automática de sistemas. No entanto, apesar de poder lidar com verificações complexas, as ferramentas de verificação de modelos usualmente não fornecem informação alguma sobre como reparar inconsistências nestes modelos. Nesta dissertação, mostramos que abordagens desenvolvidas para a atualização de modelos CTL inconsistentes não são capazes de lidar com todos os tipos de alterações em modelos. Introduzimos então o conceito de revisão de modelos: uma abordagem baseada em revisão de crenças para o reparo de modelos inconsistentes em um contexto estático. Relacionamos nossa proposta com trabalhos clássicos em revisão de crenças. Definimos um operador de revisão de modelos e mostramos que este obedece postulados de racionalidade clássico de revisão de crenças. Propomos um algoritmo de revisão com base no algoritmo utilizado pela abordagem de atualização de modelos. Discutimos sobre problemas e limites do algoritmo proposto, e mostramos que essa estratégia de adaptação não é uma solução apropriada. / Model checking is one of the most robust techniques in automated system verification. But, although this technique can handle complex verifications, model checking tools usually do not give any information on how to repair inconsistent system models. In this dissertation, we show that approaches developed for CTL model update cannot deal with all kinds of model changes. We introduce the concept of CTL model revision: an approach based on belief revision to handle system inconsistency in a static context. We relate our proposal to classical works on belief revision. We define an operator for model revision and we show that it obeys the classical rationality postulates of belief revision. We propose an algorithm for model revision based on the algorithm used by the model update approach. We discuss problems and limitations of our proposed algorithm and show that this strategy of adaptation is not an appropriate solution.

A verificação funcional é o conjunto de tarefas destinado a descobrir erros gerados durante o projeto de circuitos integrados, e representa um importante desafio ao influenciar fortemente a eficiência do ciclo inteiro de produção. Estima-se que até 80% dos custos totais de projeto são devidos à verificação, tornando esta atividade o gargalo principal para reduzir o time-to-market. Tal problemática tem provocado a aparição de diversas estratégias para diminuir o esforço, ou para aumentar a capacidade de cobertura da verificação. Por um lado existe a simulação, que permite descobrir um número razoável de erros de projeto; porém, a lentidão da simulação de descrições RTL torna mínima a cobertura real de estados. Por outro lado, os métodos formais de verificação fornecem alta cobertura de estados. Um deles é a checagem de modelos, que checa a validade de um conjunto de propriedades para todos os estados do projeto sob verificação. No entanto, esta técnica padece do problema de explosão de estados, e da dificuldade de especificar um conjunto robusto de propriedades. Outra alternativa formal é a checagem de equivalência que, ao invés de verificar propriedades, compara o projeto com um modelo de referência. No entanto, a checagem de equivalência tradicional é aplicável, unicamente, a descrições no mesmo nível de abstração, e com interfaces idênticas. Como fato importante, não foram encontrados registros na literatura de sobre a verificação formal de descrições RTL, considerando ambos os aspectos computacionais (presentes no modelo de referência) e de comunicação às interfaces (provenientes da especificação funcional de protocolo). Neste trabalho apresenta-se uma metodologia de verificação formal, através do uso de técnicas de checagem de equivalência para determinar a validade de uma implementação em RTL, comparando-a com um modelo de referência em alto nível, e com um modelo formal do protocolo de comunicação. Para permitir tal checagem, a metodologia baseia-se no conceito de sequências de estados, ao invés de estados individuais como na checagem de equivalência tradicional. As discrepâncias entre níveis diferentes de abstração são consideradas, incluindo alfabetos diferentes, mapeamento entre estados, e dessemelhanças temporais. A caracterização e solução do problema são desenvolvidas através de um quadro teórico, onde se apresentam conceitos, e definições, cuja validade é provada formalmente. Uma ferramenta para aplicação prática da metodologia foi desenvolvida e aplicada sobre diferentes tipos de descrições RTL, escritas nas linguagens VHDL e SystemC. Os resultados demonstram efetividade e eficiência na verificação formal de circuitos digitais que incluem, mas não se limitam à correção de erros, encriptação, processamento de imagens, e funções matemáticas. Também, evidencia-se a capacidade da ferramenta para descobrir erros de tipo combinatório e sequencial injetados propositalmente, relacionados com a funcionalidade do modelo de referência, assim como, com a da especificação do protocolo de comunicação, dentro de tempos e número de iterações praticáveis em casos reais. / Functional verification is the group of tasks aiming the discovery of bugs created during integrated circuit design, and represents an important challenge by its strong influence on efficiency throughout production cycles. As an estimative, up to 80% of the whole design costs are due to verification, which makes verification the greatest bottleneck while attempting to reduce time-to-market. Such problem has given rise to a series of techniques to reduce the effort, or to increase verification coverage capability. On the one side, simulation allows finding a good number of bugs, but it is still far from reaching high state coverage because of RTL cycle-accurate slowness. On the other side, formal approaches supply high state coverage. Model checking, for instance, checks the validness of a set of properties for all designs states. However, a strong disadvantage resides in defining and determining the quality of the set of properties to verify, not to mention state explosion. Sequential equivalence checking, which instead of checking properties compares the design with a reference model. Nevertheless, traditionally it can only be applied between circuit descriptions where a one-to-one correspondence for states, as well as for memory elements, is expected. As a remarkable issue, no works were found in literature that dealt with formal verification of RTL designs, while taking care of both computational aspects, present in the high-level reference model, and interface communication aspects, which proceed from the protocol functional specification. This work presents a formal verification methodology, which uses equivalence checking techniques, to validate RTL descriptions through direct comparison with a high-level reference model, and with formal model of the communication protocol. It is based on extracting and comparing complete sequences of states, instead of single states as in traditional equivalence checking, in order to determine if the design intention is maintained in RTL implementation. The natural discrepancies between system level and RTL code are considered, including non-matching interface and memory elements, state mapping, and process concurrency. For the complete problem characterization and solution, a theoretical framework is introduced, where concepts and definitions are provided, and whose validity is formally proved. A tool to apply systematically the methodology was developed and applied on different types of RTL descriptions, written in VHDL and SystemC languages. The results show that the approach may be applied effectively and efficiently to verify formally digital circuits that include, but are not limited to error correction, encryption, image processing, and math functions. Also, evidence has been obtained about the capacity of the tool to discover both combinatory and sequential bugs injected on purpose, related with computational and protocol functionalities, on real scenarios.

A verificação funcional é o conjunto de tarefas destinado a descobrir erros gerados durante o projeto de circuitos integrados, e representa um importante desafio ao influenciar fortemente a eficiência do ciclo inteiro de produção. Estima-se que até 80% dos custos totais de projeto são devidos à verificação, tornando esta atividade o gargalo principal para reduzir o time-to-market. Tal problemática tem provocado a aparição de diversas estratégias para diminuir o esforço, ou para aumentar a capacidade de cobertura da verificação. Por um lado existe a simulação, que permite descobrir um número razoável de erros de projeto; porém, a lentidão da simulação de descrições RTL torna mínima a cobertura real de estados. Por outro lado, os métodos formais de verificação fornecem alta cobertura de estados. Um deles é a checagem de modelos, que checa a validade de um conjunto de propriedades para todos os estados do projeto sob verificação. No entanto, esta técnica padece do problema de explosão de estados, e da dificuldade de especificar um conjunto robusto de propriedades. Outra alternativa formal é a checagem de equivalência que, ao invés de verificar propriedades, compara o projeto com um modelo de referência. No entanto, a checagem de equivalência tradicional é aplicável, unicamente, a descrições no mesmo nível de abstração, e com interfaces idênticas. Como fato importante, não foram encontrados registros na literatura de sobre a verificação formal de descrições RTL, considerando ambos os aspectos computacionais (presentes no modelo de referência) e de comunicação às interfaces (provenientes da especificação funcional de protocolo). Neste trabalho apresenta-se uma metodologia de verificação formal, através do uso de técnicas de checagem de equivalência para determinar a validade de uma implementação em RTL, comparando-a com um modelo de referência em alto nível, e com um modelo formal do protocolo de comunicação. Para permitir tal checagem, a metodologia baseia-se no conceito de sequências de estados, ao invés de estados individuais como na checagem de equivalência tradicional. As discrepâncias entre níveis diferentes de abstração são consideradas, incluindo alfabetos diferentes, mapeamento entre estados, e dessemelhanças temporais. A caracterização e solução do problema são desenvolvidas através de um quadro teórico, onde se apresentam conceitos, e definições, cuja validade é provada formalmente. Uma ferramenta para aplicação prática da metodologia foi desenvolvida e aplicada sobre diferentes tipos de descrições RTL, escritas nas linguagens VHDL e SystemC. Os resultados demonstram efetividade e eficiência na verificação formal de circuitos digitais que incluem, mas não se limitam à correção de erros, encriptação, processamento de imagens, e funções matemáticas. Também, evidencia-se a capacidade da ferramenta para descobrir erros de tipo combinatório e sequencial injetados propositalmente, relacionados com a funcionalidade do modelo de referência, assim como, com a da especificação do protocolo de comunicação, dentro de tempos e número de iterações praticáveis em casos reais. / Functional verification is the group of tasks aiming the discovery of bugs created during integrated circuit design, and represents an important challenge by its strong influence on efficiency throughout production cycles. As an estimative, up to 80% of the whole design costs are due to verification, which makes verification the greatest bottleneck while attempting to reduce time-to-market. Such problem has given rise to a series of techniques to reduce the effort, or to increase verification coverage capability. On the one side, simulation allows finding a good number of bugs, but it is still far from reaching high state coverage because of RTL cycle-accurate slowness. On the other side, formal approaches supply high state coverage. Model checking, for instance, checks the validness of a set of properties for all designs states. However, a strong disadvantage resides in defining and determining the quality of the set of properties to verify, not to mention state explosion. Sequential equivalence checking, which instead of checking properties compares the design with a reference model. Nevertheless, traditionally it can only be applied between circuit descriptions where a one-to-one correspondence for states, as well as for memory elements, is expected. As a remarkable issue, no works were found in literature that dealt with formal verification of RTL designs, while taking care of both computational aspects, present in the high-level reference model, and interface communication aspects, which proceed from the protocol functional specification. This work presents a formal verification methodology, which uses equivalence checking techniques, to validate RTL descriptions through direct comparison with a high-level reference model, and with formal model of the communication protocol. It is based on extracting and comparing complete sequences of states, instead of single states as in traditional equivalence checking, in order to determine if the design intention is maintained in RTL implementation. The natural discrepancies between system level and RTL code are considered, including non-matching interface and memory elements, state mapping, and process concurrency. For the complete problem characterization and solution, a theoretical framework is introduced, where concepts and definitions are provided, and whose validity is formally proved. A tool to apply systematically the methodology was developed and applied on different types of RTL descriptions, written in VHDL and SystemC languages. The results show that the approach may be applied effectively and efficiently to verify formally digital circuits that include, but are not limited to error correction, encryption, image processing, and math functions. Also, evidence has been obtained about the capacity of the tool to discover both combinatory and sequential bugs injected on purpose, related with computational and protocol functionalities, on real scenarios.

O objetivo do trabalho é analisar os protocolos mais conhecidos de medição e verificação de programas de eficiência energética sob da ótica a aplicação do recurso privado em projetos de eficiência energética. A simples comparação de faturas de energia e a utilização não rigorosa de indicadores para determinação da energia economizada praticamente deixa de ser uma opção com a disponibilização de padrões compreensivos de M&V. Para tal são analisados estudos de caso de projetos de eficiência energética nos segmentos comercial e industrial e estes indicam um distanciamento entre as ferramentas modernas de M&V e a realidade, de modo que há dúvidas sobre garantia da sustentabilidade das ações ao longo do tempo. Dessa análise dos protocolos e estudos de caso foram identificadas demandas que são partes de uma metodologia proposta em 9 etapas focadas na sustentabilidade da energia economizada. A aplicação dessa metodologia é complementar à aplicação dos protocolos, tal que o engenheiro de eficiência energética possa pensar em todo processo de gestão e não apenas na implementação das MCEs. Esse trabalho conclui que a simples aderência aos protocolos de M&V é insuficiente para garantir a sustentabilidade das ações de conservação de energia a longo prazo. / The purpose of this work is to analyze the most well known Measurement and Verification protocols to energy efficiency programs under private capital owner perspective. The simple comparison between energy bills and the non-rigorous use of energy efficiency indicators in the energy savings calculation are not an option anymore with the introduction of comprehensive M&V protocols. With this aim, energy efficiency case studies are analyzed in the commercial and industrial sectors and indicated theres a gap between the modern M&V tools and the reality. Doubts around the sustainability of energy savings in the long term raised. Based on literature review, analysis of protocols and case studies, improvement opportunities were identified and are part of a 9 steps methodology focused on the sustainability of energy savings proposed in this work. This methodology works in cooperation with current M&V protocols. The EE engineer shall then be able to think in the overall management process and not only in the Energy Conservation Measure. This work concluded that the M&V tools adherence solely is insufficient to guarantee the sustainability of energy savings in the long term.

Uma das maiores restrições que existe atualmente no fluxo de projeto de CIs é a necessidade de um ciclo menor de desenvolvimento. Devido às grandes dimensões dos sistemas atuais, é muito provável encontrar no projeto de blocos IP, erros ou bugs originados na passagem de uma dada especificação inicial para seus correspondentes modelos de descrição de hardware. Isto faz com que seja necessário verificar tais modelos para garantir aplicações cem por cento funcionais. Uma das técnicas de verificação que tem adquirido bastante popularidade recentemente é a verificação funcional, uma vez que é uma alternativa que ajuda a manter baixos custos de validação dos modelos HDL ao longo do projeto completo do circuito. Na verificação funcional, que está baseada em ambientes de simulação, a funcionalidade completa (ou relevante) do modelo é explorada, aplicando-se casos de teste, um após o outro. Isto permite examinar o modelo em todas as seqüências e combinações de entradas desejadas. Na verificação funcional, existe a possibilidade de simular o modelo estimulando-o com casos de teste aleatórios, o qual ajuda a cobrir um amplo número de estados. Para facilitar a aplicação de estímulos em simulação de circuitos, é comum que espaços definidos por parâmetros de entrada sejam limitados em sua abrangência e agrupados de tal forma que subespaços sejam formados. No desenvolvimento de testbenches, os geradores de estímulos aleatórios podem ser criados de forma a conter subespaços que se sobrepõem (resultando em estímulos redundantes) ou subespaços que contenham condições que não sejam de interesse (resultando em estímulos inválidos). É possível eliminar ou diminuir, os casos de teste redundantes e inválidos através da aplicação de metodologias de modificação do espaço de estímulos de entrada, e assim, diminuir o tempo requerido para completar a simulação de modelos HDL. No presente trabalho, é realizada uma análise da aplicação da técnica de organização do espaço de entrada através de domínios de parâmetros do IP, e uma metodologia é desenvolvida para tal, incluindo-se, aí, uma ferramenta de codificação automática de geradores de estímulos aleatórios em linguagem SyatemC: o GET_PRG. Resultados com a aplicação da metodologia é comparada a casos de aplicação de estímulos aleatórios gerados a partir de um espaço de estímulos de entrada sem modificações.Como esperado, o número de casos de teste redundantes e inválidos aplicados aos testbenches foi sempre maior para o caso de estimulação aleatória a partir do espaço de estímulos de entrada completo com um tempo de execução mais longo. / One of the strongest restrictions that exist throughout ICs design flow is the need for shorter development cycles. This, along with the constant demand for more functionalities, has been the main cause for the appearance of the so-called System-on-Chip (SOC) architectures, consisting of systems that contain dozens of reusable hardware blocks (Intellectual Properties, or IPs). The increasing complexity makes it necessary to thoroughly verify such models in order to guarantee 100% functional applications. Among the current verification techniques, functional verification has received important attention, since it represents an alternative that keeps HDL validation costs low throughout the circuits design cycle. Functional verification is based in testbenches, and it works by exploring the whole (or relevant) models functionality, applying test cases in a sequential fashion. This allows the testing of the model in all desired input sequences and combinations. There are different techniques concerning testbench design, being the random stimulation an important approach, by which a huge number of test cases can be automatically created. In order to ease the stimuli application in circuit simulation, it is common to limit the range of the space defined by input parameters and to group such restricted parameters in sub-spaces. In testbench development, it may occur the creation of random stimuli generators containing overlapping sub-spaces (resulting in redundant stimuli) or sub-spaces containing conditions of no interest (resulting in invalid stimuli). It is possible to eliminate, or at least reduce redundant and invalid test cases by modifying the input stimuli space, thus, diminishing the time required to complete the HDL models simulation. In this work, the application of a technique aimed to organize the input stimuli space, by means of IP parameter domains, is analyzed. A verification methodology based on that is developed, including a tool for automatic coding of random stimuli generators using SystemC: GET_PRG. Results on applying such a methodology are compared to cases where test vectors from the complete verification space are generated. As expected, the number of redundant test cases applied to the testbenches was always greater for the case of random stimulation on the whole (unreduced, unorganized) input stimuli space, with a larger testbench execution time.

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.

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.

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.