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.

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.

Em decorrência de sua atuação expressiva no mercado de financiamento de empreendimentos de habitação e infraestrutura, a Caixa Econômica Federal (Caixa) é um banco de grande relevância para o setor da construção civil brasileira. A Caixa mantém um setor técnico no qual são desempenhadas, dentre demais responsabilidades, as atividades de análise de documentação técnica e verificação da execução orçamentária e financeira das obras. Atualmente, esses procedimentos são realizados essencialmente de forma manual, configurando um processo moroso e suscetível à ocorrência de imprecisões. Nesse sentido, o presente trabalho tem como objetivo analisar a introdução da Modelagem da Informação da Construção, notadamente, no processo de verificação da documentação técnica de obras, realizado pelos profissionais desse banco público. Primeiramente, realizou-se um diagnóstico, por meio de uma survey, no setor técnico da Caixa que apontou aspectos relevantes à gestão de mudanças de origem tecnológica nesse ambiente. Em continuidade ao estudo de caso, investigou-se as motivações, os benefícios almejados e as possíveis barreiras para a implantação dessa inovação no processo de análise técnica desenvolvido pela instituição. Para verificar a adequabilidade e a aceitação das propostas preliminares de ferramentas e diretrizes de modelagem foi conduzido um workshop no qual participaram profissionais voluntários do mercado da construção civil. Com base neste estudo, apresentado neste trabalho na forma de três artigos científicos publicados, verificou-se que a Caixa pode ser considerada um importante vetor de difusão de práticas associadas à Modelagem da Informação da Construção na indústria da construção civil brasileira e que a proposição de novas ferramentas e diretrizes poderia ser efetivamente adequada para incrementar a prática projetual. Além disso, observou-se que a transformação interna necessária para a implementação de mudanças nos processos técnicos da Caixa é viável desde que seja propiciado um ambiente favorável, em que os gestores incentivem, planejem e deem suporte às possíveis mudanças. Finalmente, a contribuição pretendida com esta pesquisa é fomentar outras iniciativas e colaborar para a disseminação da Modelagem da Informação da Construção nos setores de projeto e construção civil brasileiros. / Due to its outstanding performance in housing and infrastructure construction financing market, Caixa Econômica Federal (Caixa) is a bank of great importance in the Brazilian Construction and Design industry. Caixa maintains a technical department that, among other activities, perform technical feasibility analyses, and verify the budgetary and financial development of construction projects. Currently, the project analysis process is manual, time-consuming and error-prone. In this sense, the present study aims to analyse the introduction of Building Information Modelling in the technical feasibility analyses process, carried out by engineers and architects. Firstly, a survey was conducted to perform an intraorganizational assessment of Caixa\'s technical department, in order to identify aspects relevant to change management. Secondly, in this study case, the motivations, the desired benefits and potential barriers to the implementation of this innovation were investigated. In addition, a workshop was conducted with construction and design professionals to verify the suitability and acceptance of the preliminary proposals of tools and modelling guidelines. Based on this study presented in three published scientific papers, Caixa can be considered an important diffusion vector of Building Information Modelling practices in the Brazilian construction and design industry. In addition, the proposition of new tools and modelling guidelines could effectively be appropriate to enhance its design practices. Furthermore, the intraorganizational change required for implementing innovations in the Caixa technical department proved to be feasible if provided with a favourable environment in which managers stimulate, plan and support possible changes. Finally, the intended contribution of this research is to encourage other initiatives and contribute to spreading additional practices related to Building Information Modelling in the Brazilian construction and design industry.

A UML (Unified Modeling Language) é uma linguagem de modelagem para especificar, construir e documentar artefatos de sistemas de software. A UML-RT, usada pela ferramenta Rational Rose RealTime (RoseRT), é uma extensão da UML que permite a modelagem de sistemas de tempo real distribuídos e guiados por evento. A UML-RT não possui semântica formal, logo não é possível realizar verificação formal do modelo. O presente trabalho propõe o mapeamento dos elementos de comunicação da UML-RT para a álgebra de processos p-calculus, a fim de prover semântica formal à UML-RT. Com objetivo de automatizar o mapeamento, foi desenvolvido um protótipo de tradutor que captura o modelo UML-RT especificado na ferramenta RoseRT e determina suas definições p-calculus. As definições p-calculus geradas utilizam a sintaxe da gramática do HAL-JACK, que é uma ferramenta integrada para verificação e análise de sistemas expressos em p-calculus, assim as definições p-calculus podem ser submetidas ao HAL-JACK para verificação formal de propriedades. Este trabalho detalha o mapeamento UML-RT para p-calculus, descreve o protótipo desenvolvido e apresenta alguns exemplos do mapeamento do modelo UML-RT para definições p-calculus.

Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely re exive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as an MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., \"every time the agent does X, it will do Y later\"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS\'s and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or an inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose with respect to the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again. In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into an MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach. / Sistemas multi-agentes (SMAs) podem ser usados para modelar fenômenos que podem ser decompostos em diversos agentes que interagem entre si dentro de um ambiente. Em particular, eles podem ser usados para modelar sociedades humanas e animais, com a finalidade de se analisar as suas propriedades computacionalmente. Esta tese trata da análise automatizada de um tipo particular de tais modelos sociais, a saber, aqueles baseados em princípios behavioristas, o que contrasta com as abordagens cognitivas mais dominante na literatura de SMAs. A principal característica das teorias behaviorista é a ênfase na descrição do comportamento em termos da interação entre agentes e seu ambiente. Desta forma, não apenas ações refl exivas, mas também de aprendizado, motivações, e as emoções podem ser definidas. Mais especificamente, nesta tese apresentamos uma arquitetura de agentes formal (especificada através da Notação Z) baseada na teoria da Análise do Comportamento de B. F. Skinner, e fornecemos uma noção adequada e formal de ambiente (com base na álgebra de processos pi-calculus) para colocar tais agentes juntos em um SMA. Simulações são freqüentemente utilizadas para se analisar SMAs. As técnicas envolvidas tipicamente consistem em simular um SMA diversas vezes, seja para coletar estatísticas, seja para observar o que acontece através de animações. Contudo, simulações podem ser usadas de forma a pertmitir a realização de verificações automatizadas do SMA caso sejam entendidas como explorações de grandes espaços-de-estados. Nesta tese propomos uma técnica de verificação baseada nessa observação, que consiste em simular um SMA de uma forma guiada, a fim de se determinar se uma dada hipótese sobre ele é verdadeira ou não. Para tal fim, tiramos proveito da importância que os ambientes têm nesta tese: a especificação formal do ambiente de um SMA serve para calcular as evoluções possíveis do SMA como um sistema de transição, estabelecendo assim o espaço-de-estados a ser investigado. Neste cálculo, os agentes são levados em conta simulando-os, a fim de determinar, em cada estado do ambiente, quais são suas ações. Cada execução da simulação é uma seqüência de estados nesse espaço-de-estados, que é calculado em tempo de execução, conforme a simulação progride. A hipótese a ser investigada, por sua vez, é dada como um outro sistema de transição, chamado propósito de simulação, o qual define as simulações desejáveis e indesejáveis (e.g., \"sempre que o agente fizer X, ele fará Y depois\"). Em seguida, é possível verificar se o SMA satisfaz o propósito de simulação de acordo com uma série de relações de satisfatibilidade precisamente definidas. Algoritmicamente, isso corresponde a construir um produto síncrono desses dois sistemas de transições (i.e., o do SMA e o do propósito de simulação) em tempo de execução e usá-lo para operar um simulador. Ou seja, o propósito de simulação é usado para guiar o simulador, de modo que somente os estados relevantes sejam efetivamente simulados. Ao terminar, um tal algoritmo pode fornecer um veredito conclusivo ou inconclusivo. Se conclusivo, descobre-se se o SMA satisfaz ou não o propósito de simulação com relação às observações feitas durante as simulações. Se inconclusivo, é possível realizar alguns ajustes e tentar novamente. em resumo, portanto, nesta tese propomos quatro novos elementos: (i) uma arquitetura de agente, (ii) uma especificação formal do ambiente desses agentes, de modo que possam ser compostos em um SMA, (iii) uma estrutura para descrever a propriedade de interesse, a qual chamamos de propósito de simulação, e (iv) uma técnica para se analisar formalmente o SMA resultante com relação a um propósito de simulação. Esses elementos estão implementados em uma ferramenta, denominada Simulador Formalmente Guiado (FGS, do inglês Formally Guided Simulator). Estudos de caso executáveis no FGS são fornecidos para ilustrar a abordagem.

O teste de software engloba diferentes técnicas, métodos e conceitos capazes de garantir a qualidade dos mais variados tipos de sistemas. Dentre tais técnicas, encontra-se o teste baseado em Máquinas de Estados Finitos (MEFs), que visa a garantir a conformidade entre a implementação e a especificação de um software. Com esse propósito, diversos métodos foram propostos para a geração de seqüências de verificação que garantam cobertura total das possíveis falhas existentes em uma implementação. A maioria dos métodos conhecidos são baseados na utilização de seqüências de distinção. Esse recurso, porem, não existe para toda MEF. Alguns métodos buscam a geração de seqüências de verificação baseados em recursos alternativos as seqüências de distinção, contudo, as seqüências geradas são exponencialmente longas. Este trabalho apresenta um método para geração de seqüências de verificação que visa a reduzir o tamanho das seqüências geradas para o domínio de MEFs que não dispõem de seqüência de distinção. Para isso, o método proposto baseia-se na utilização de conjuntos de distinção. Uma avaliação experimental foi realizada afim de mensurar a redução proporcionada pelo método proposto em relação aos principais métodos existentes na literatura. Com esse intuito, foram geradas MEFs aleatórias sob a perspectiva diferentes fatores. Em relação a variação do número de estados, os resultados indicaram reduções acima de 99; 5% em comparação com os métodos existentes, quando analisadas 75% das MEFs geradas / Software testing involves several techniques, methods, and concepts employed to guarantee a high level of quality in different application domains. Among such techniques, Finite State Machine (FSM) based testing aims to guarantee the conformance between the implementation and the specification of a system under test. In this context, several methods were proposed to generate checking sequences that cover all the possible faults existing in an implementation. Most of these methods are based on a special sequence, named distinguishing sequence, which does not exist for every minimal machine. Some methods were proposed to generate checking sequences based on alternative solutions in order to be applied on FSMs that do not have distinguishing sequences. However, these methods generate checking sequences exponentially long. This work proposes a method to generate checking sequences using identification sets. These sets exist for every minimal FSM and also lead to shorter checking sequences. We conducted an experimental study to compare the proposed method with the main existing methods. In the experiments, we used random FSMs that have different configurations of states, inputs, and outputs. Concerning the variation of number of states, the results show reductions higher than 99:5% in comparison with the existing methods for 75% of the experimented machines

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.

Advances in communicat ions have been unarguably essent ial to enablemodern systems and applicat ions as we know them. Ubiquity has turned into reality, allowing specialised embedded systems to eminent ly grow and spread. That is notably the case of unmanned vehicles which have been creat ively explored on applications that were not as efficient as they currently are, neither as innovative as recent ly accomplished. Therefore, towards the efficient operat ion of either unmanned vehicles and systems they integrate, in addition to communicat ion improvements, it is highly desired that we carefully observe relevant , co-related necessit ies that may lead to the full insert ion of unmanned vehicles to our everyday lives. Moreover, by addressing these demands on integrated solut ions, better resultswill likely be produced. This thesis presentsHAMSTER, theHeAlthy, Mobility and Security based data communication archiTEctuRe for unmanned vehicles, which addresses threemain types of communicat ions: machine-to-machine, machine-to-infrast ructure and internal machine communications. Four addit ional elements on co-related requirements are provided alongside with HAMSTER for more accurate approaches regarding security and safety aspects (SPHERE platform), crit icality analysis (NCI index), energy efficiency (NP plat form) and mobility-oriented ad hoc and infrast ructured communicat ions (NIMBLE platform). Furthermore, three specialised versions are provided: unmanned aerial vehicles (Flying HAMSTER), unmanned ground vehicles (Running HAMSTER) and unmanned surface/ underwater vehicles (Swimming HAMSTER). The architecture validat ion is achieved by case studies on each feature addressed, leading to guidelines on the development of vehicles more likely to meet certificat ion requirements, more efficient and secure communicat ions, assert ive approaches regarding crit icality and green approaches on internal communicat ions. Indeed, results prove the efficiency and effectiveness of HAMSTER architecture and its elements, as well as its flexibility in carrying out different experiments focused on various aspects of communication, which helps researchers and developers to achieve safe and secure communicat ions in unmanned vehicles. / Os avanços na área de comunicações foram indiscutívelmente essenciais para a obtenção de sistemas e aplicações modernos como os o atuais. A computação ubíqua se tornou realidade, permitindo que sistemas embarcados especializados ganhassem espaço e cada vez mais autonomia. Esse é notavelmente o caso de veículos não tripulados que têm sido criativamente explorados em aplicações inovadoras e avançadas. Entretanto, para o funcionamento eficiente desses veículos e sistemas não tripulados, além de melhorias de comunicação, é altamente desejável que as necessidades relevantes co-relacionadas a comunica¸cao sejam cuidadosamente observadas, levando a uma facilitação na inserção de veículos não tripulados em espaços públicos. Além disso, ao abordar essas demandas de modo integrado, as chances de produzir melhores resultados é maior. Esta tese apresenta a HAMSTER, uma arquitetura de comunicação de dados baseada em mobilidade e segurança para veículos não tripulados, que aborda três tipos principais de comunicação: máquina-para- máquina, máquina-para-infraestrutura e comunicações internas. Quatro elementos adicionais co-relacionados são fornecidos juntamente com a arquitetura HAMSTER de modo a prover abordagens mais precisas em relação a aspectos de segurança física e da informação (plataforma SPHERE), análise de criticalidade (índice NCI), eficiência energética (plataforma NP) e comunicações ad hoc e infraestruturadas orientadas a mobilidade (plataforma NIMBLE). Além disso, são fornecidas três versões especializadas: para veículos aéreos não tripulados (Flying HAMSTER), veículos terrestres não tripulados (Running HAMSTER) e veículos submarinos e de superfície não tripulados (Swimming HAMSTER). A validação da arquitetura é obtida por meio de estudos de caso sobre cada recurso abordado, levando a diretrizes sobre o desenvolvimento de veículos mais preparados para atender a requisitos de certificação, comunicação mais eficiente e segura, abordagens assertivas sobre criticidade e abordagens verdes nas comunicações internas. Por fim, os resultados comprovaram a eficiência da arquitetura HAMSTER e os elementos com ela providos, bem como a flexibilidade em realizar experimentos focados em vários aspectos de comunicação, auxiliando na obtenção de comunicações seguras em veículos autônomos.

A segurança do paciente cirúrgico é problemática complexa e desafiadora em âmbito global. A presente pesquisa teve como objetivos (a) analisar as evidências disponíveis na literatura sobre o processo de implementação da lista de verificação de segurança cirúrgica da Organização Mundial da Saúde na prática dos serviços de saúde, e (b) analisar o processo de implementação e o uso diário da lista de verificação de segurança cirúrgica, segundo o relato de enfermeiros que atuavam em unidades de centro cirúrgico de hospitais de duas cidades localizadas no estado do Paraná. A pesquisa foi conduzida em duas fases: revisão integrativa e estudo descritivo. A busca dos estudos primários foi realizada nas bases de dados PubMed, CINAHL e LILACS. A amostra da revisão integrativa foi composta de 27 pesquisas agrupadas em três categorias, a saber: processo de implementação: estratégias para introdução da lista de verificação de segurança cirúrgica nos serviços de saúde (n=15); processo de implementação: estratégias para otimização do uso da lista de verificação de segurança cirúrgica nos serviços de saúde (n=9) e facilitadores e barreiras para implementação da lista de verificação de segurança cirúrgica nos serviços de saúde (n=3). A condução da revisão integrativa possibilitou compreender o processo de implementação da lista, as diferentes estratégias utilizadas para sua implantação, aspectos da implementação considerados bem-sucedidos ou pouco exitosos no alcance dos resultados esperados, facilitadores e barreiras deste processo. O estudo descritivo foi realizado em 25 hospitais de duas cidades que compõem a mesorregião do Norte Central Paranaense (Londrina e Maringá). Os participantes foram 91 enfermeiros que atuavam em centro cirúrgico dos hospitais selecionados. Para a coleta de dados elaborou-se dois instrumentos, os quais foram submetidos à validação aparente e de conteúdo. Os resultados evidenciaram que, na maioria dos hospitais investigados, a lista de verificação de segurança cirúrgica foi implementada, sendo que, para a maioria dos participantes, as estratégias adotadas na introdução da lista foram o planejamento prévio conduzido pelos enfermeiros, a adaptação com predominância do uso no formato impresso e programa educacional. Com relação ao uso diário da lista, a maioria dos enfermeiros apontou a utilização inadequada desta prática nos seguintes aspectos: adesão parcial ao uso pela equipe cirúrgica, diferença de adesão entre as etapas de checagem e entre as categorias profissionais e condutas inadequadas da equipe cirúrgica na checagem da lista em sala cirúrgica (equipe incompleta, desatenta e sem participação ativa de seus membros). Para a maioria dos participantes, o uso da lista trouxe benefícios ou tem potencial para produzir efeitos benéficos para o paciente, equipe cirúrgica e serviço de saúde. As evidências geradas trazem subsídios para os enfermeiros e demais profissionais de saúde na elaboração de protocolos relativos ao processo de implementação ou uso diário da lista mais adequados e compatíveis com as especificidades estruturais e organizacionais dos serviços de saúde nacionais, com o propósito de viabilizar a integração desta ferramenta no processo de trabalho, melhorar a adesão da equipe e alcançar os melhores resultados em prol da segurança do paciente / Surgical patient safety is a complex and challenging problem at the global level. This study aimed to analyze (a) the available evidence in the literature on the process of implementation of the surgical safety checklist of the World Health Organization in the practice of health services, and (b) the implementation process and the daily use of the surgical safety checklist, according to the report of nurses working in surgical center units of hospitals of two cities located in the state of Paraná. The research was conducted in two phases: integrative review and descriptive study. The search for primary studies was carried out in PubMed, CINAHL and LILACS databases. The sample of the integrative review consisted of 27 studies grouped into three categories, namely: implementation process: strategies for the introduction of the surgical safety checklist in the health services (n = 15); implementation process: strategies to optimize the use of the surgical safety checklist in health services (n = 9) and facilitators and barriers to the implementation of the surgical safety checklist (n = 3). Conducting the integrative review made it possible to understand the process of implementing the list, the different strategies used for its implementation, aspects of implementation considered successful or not very successful in achieving the expected results, facilitators and barriers of this process. The descriptive study was carried out in 25 hospitals of two cities that make up the mesoregion of Northern Central of Paraná state (Londrina and Maringá). Participants were 91 nurses who worked in the surgical center of the selected hospitals. For the data collection, two instruments were elaborated, which were submitted to the apparent validation and content. The results showed that, in most of the hospitals investigated, the surgical safety checklist was implemented, and, for most of the participants, the strategies adopted in the introduction of the list were the previous planning conducted by the nurses, the adaptation with predominance of the use in the printed format and educational program. Regarding the daily use of the list, most of the nurses pointed out the inadequate use of this practice in the following aspects: surgical team\'s partial adherence to the use of it, difference in adherence between the check-up stages, and between the professional categories and inadequate behavior of the surgical team in checking the list in the surgical room (incomplete, inattentive team, and members not taking part actively). For most participants, using the list has brought benefits or can potentially produce beneficial effects for the patient, surgical team, and health service. The evidence generated provides subsidies for nurses and other health professionals in elaborating protocols related to the implementation process or daily use of the list more adequate and compatible with the structural and organizational specificities of the national health services, in order to make feasible the integration of this tool into the work process, to improve team adherence and to achieve the best results for patient safety

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.