Proventricular dilatation disease (PDD) was first recognized during an outbreak among captive macaws in the late 1970s. The disease, also known as proventricular dilatation syndrome or macaw wasting disease can occur in any psittacine but the most commonly affected birds are macaws, cockatoos and conures. The disease causes inflammation of the central, peripheral and autonomic nervous systems, as well as weight loss associated with regurgitation and the passage of undigested food in the feces. Although a viral etiology for PDD has been suspected for almost 40 years, the etiologic agent of the disease was unknown until lately. Recently we cultured a novel bornavirus from brain tissue from birds clinically diagnosed with PDD. This finding supports data from other groups who, in 2008, identified bornavirus sequences among birds suffering from PDD. It was reported that more 60 percent of PDD affected birds were infected with the new virus, designated avian bornavirus (ABV). ABV is a negative sense, single stranded RNA virus related to Borna disease virus (BDV). ABV isolates differ dramatically from BDV isolates in their level of genetic variation. Using polymerase chain reaction (PCR) assays, we were able to detect ABV in feces and tissue of PDD birds. We also detected ABV shedding from clinically healthy birds housed in aviaries with no history of the disease. We also determined the complete genome sequences of eight North American ABV isolates. Genotyping indicates that the majority of North American ABV isolates are genotype 4. We found one ABV, genotype 1, which is the first complete sequencing of this genotype. Moreover, we found ABV genotype 2, isolated from an apparently healthy cockatiel with no PDD clinical signs. In order to investigate whether this genotype is avirulent, the virus was grown in duck embryo fibroblasts and inoculated into two adult cockatiels by the oral and intramuscular routes. One bird developed clinical signs on day 33 and was euthanized on day 36. The second challenged bird developed clinical signs on day 41 and was euthanized on day 45. On necropsy, the proventriculus of both birds was slightly enlarged and microscopic examination showed lesions consistent with PDD in the brain, spinal cord, heart, adrenal gland and intestine. A control, uninoculated cockatiel was apparently healthy when euthanized on day 50. ABV2 is now the second ABV genotype to be formally shown to cause PDD.

Os vírus são patógenos importantes na saúde das aves, podendo levar a surtos que ameaçam de forma significante a população destas. O Bornavírus aviário (ABV), o Circovírus (BFDV) e o Poliomavírus (APV) são os agentes virais mais comuns e que mais ameaçam os psitacídeos de cativeiro. O ABV é responsável pela doença da dilatação proventricular (PDD) em psitacídeos e outras aves, uma doença neurológica letal, que foi descoberta no início da década de oitenta na Europa e América do Norte. A primeira infecção por APV descrita em aves foi em periquitos australianos (Melopsittacus undulatus) jovens, sendo depois associada com elevada mortalidade e morbidade em outros psitacídeos. O BFDV é o agente causador da doença do bico e das penas de psitacídeos, que ocorre quase exclusivamente em psitacídeos, principalmente em criatórios, aves em quarentena e lojas de animais. Foram testadas 120 amostras de psitacídeos de cativeiro no Brasil, para BFDV e APV e 112 amostras para ABV, resultando em 21 (17,5%) aves positivas para APV, 41 (34,17%) para BFDV e 32 (28,57 %) para ABV. Entre os animais positivos, quatorze apresentaram infecção concomitante, sete foram positivos para BFDV e ABV, seis positivos para BFDV e APV e uma positiva para BFDV, APV e ABV. Dentre os animais positivos para BFDV, os sinais clínicos mais comuns encontrados foram apteria e apatia/anorexia, em relação às aves positivas para APV foram a apatia/anorexia, enquanto para ABV os sinais neurológicos foram os mais representados. A detecção de APV, BFDV e ABV demostra a ocorrência destes vírus testados em psitacídeos de cativeiro no Brasil, tanto em espécies exóticas como em espécies nativas. / Viruses are important pathogens in avian health and may lead to outbreaks that threaten significantly the population of birds. The Avian Bornavírus (ABV), Circovirus (BFDV) and Avian Polyomavirus (APV) are the most common viral agents that threaten parrots in captivity. The ABV is responsible for the proventricular dilation (PDD) in parrots and other birds, a lethal neurological disease, which was discovered in the early eighties in Europe and North America the disease. The first APV infection in birds has been described in young Australian budgerigars (Melopsittacus undulatus), after being associated with high mortality and morbidity in other parrots. The BFDV is the causative agent of Beak and Feathers Disease, which occurs almost exclusively in psittacines, especially in aviary, quarantine birds and pet stores. A total of 120 captivity parrots were tested in Brazil for BFDV and APV and 112 samples for ABV, resulting in 21 (17.5%) positives for APV, 41 (34.17%) for BFDV and 32 (28.57%) for ABV. Among the positive animals, fourteen had concomitant infection, six were positive for both APV and BFDV, seven for BFDV and ABV, and one sample was positive for BFDV, APV and ABV. Among BFDV positive animals, most common clinical signs were apteria and apathy/anorexia, for APV positive birds were apathy/anorexia, while for ABV were neurological signs were the most represented. The detection of APV, BFDV and ABV demostrate the occurrence of all tested viruses in captive parrots in Brazil, including exotic and native species.

Os vírus são patógenos importantes na saúde das aves, podendo levar a surtos que ameaçam de forma significante a população destas. O Bornavírus aviário (ABV), o Circovírus (BFDV) e o Poliomavírus (APV) são os agentes virais mais comuns e que mais ameaçam os psitacídeos de cativeiro. O ABV é responsável pela doença da dilatação proventricular (PDD) em psitacídeos e outras aves, uma doença neurológica letal, que foi descoberta no início da década de oitenta na Europa e América do Norte. A primeira infecção por APV descrita em aves foi em periquitos australianos (Melopsittacus undulatus) jovens, sendo depois associada com elevada mortalidade e morbidade em outros psitacídeos. O BFDV é o agente causador da doença do bico e das penas de psitacídeos, que ocorre quase exclusivamente em psitacídeos, principalmente em criatórios, aves em quarentena e lojas de animais. Foram testadas 120 amostras de psitacídeos de cativeiro no Brasil, para BFDV e APV e 112 amostras para ABV, resultando em 21 (17,5%) aves positivas para APV, 41 (34,17%) para BFDV e 32 (28,57 %) para ABV. Entre os animais positivos, quatorze apresentaram infecção concomitante, sete foram positivos para BFDV e ABV, seis positivos para BFDV e APV e uma positiva para BFDV, APV e ABV. Dentre os animais positivos para BFDV, os sinais clínicos mais comuns encontrados foram apteria e apatia/anorexia, em relação às aves positivas para APV foram a apatia/anorexia, enquanto para ABV os sinais neurológicos foram os mais representados. A detecção de APV, BFDV e ABV demostra a ocorrência destes vírus testados em psitacídeos de cativeiro no Brasil, tanto em espécies exóticas como em espécies nativas. / Viruses are important pathogens in avian health and may lead to outbreaks that threaten significantly the population of birds. The Avian Bornavírus (ABV), Circovirus (BFDV) and Avian Polyomavirus (APV) are the most common viral agents that threaten parrots in captivity. The ABV is responsible for the proventricular dilation (PDD) in parrots and other birds, a lethal neurological disease, which was discovered in the early eighties in Europe and North America the disease. The first APV infection in birds has been described in young Australian budgerigars (Melopsittacus undulatus), after being associated with high mortality and morbidity in other parrots. The BFDV is the causative agent of Beak and Feathers Disease, which occurs almost exclusively in psittacines, especially in aviary, quarantine birds and pet stores. A total of 120 captivity parrots were tested in Brazil for BFDV and APV and 112 samples for ABV, resulting in 21 (17.5%) positives for APV, 41 (34.17%) for BFDV and 32 (28.57%) for ABV. Among the positive animals, fourteen had concomitant infection, six were positive for both APV and BFDV, seven for BFDV and ABV, and one sample was positive for BFDV, APV and ABV. Among BFDV positive animals, most common clinical signs were apteria and apathy/anorexia, for APV positive birds were apathy/anorexia, while for ABV were neurological signs were the most represented. The detection of APV, BFDV and ABV demostrate the occurrence of all tested viruses in captive parrots in Brazil, including exotic and native species.

Cette thèse se situe dans le contexte de la vérification fonctionnelle des circuits intégrés complexes. L’objectif de ce travail est de créer un flot de vérification conjoint au flot de conception basé sur une technique appelée "vérification basée sur les assertions(ABV)". Le concept de base du flot est le raffinement automatique des spécifications formelles données sous la forme d’assertions PSL du niveau TLM au niveau RTL. La principale difficulté est la disparité des deux domaines : au niveau TLM, les communications sont modélisées par des appels de fonctions atomiques. Au niveau RTL, les échanges sont assurés par des signaux binaires évoluant selon un protocole de communication précis. Sur la base d’un ensemble de règles de transformation temporelles formelles, nous avons réalisé un outil permettant d’automatiser le raffinement de ces spécifications. Comme le raffinement des modèles, le raffinement des assertions n’est pas entièrement automatisable : des informations temporelles et structurelles doivent être fournies par l’utilisateur. L’outil réalise la saisie de ces informations de façon ergonomique, puis procède automatiquement à la transformation temporelle et structurelle de l’assertion. Il permet la génération d’assertions RTL mais aussi hybrides. Les travaux antérieurs dans ce domaine sont peu nombreux et les solutions proposées imposent de fortes restrictions sur les assertions considérées. À notre connaissance, le prototype que nous avons mis en oeuvre est le premier outil qui réalise un raffinement temporel fondé sur la sémantique formelle d’un langage de spécification standard (PSL). / The context of this thesis is the functional verification of complex integrated circuits.The objective of our work is to create a seamless verification flow joint to the design flowand based on a proved technique called Assertions-Based Verification (ABV). The mainchallenge of TLM to RTL refinement is the disparity of these two domains : at TLM,communications are modeled as atomic function calls handling all the exchanged data.At RTL, communications are performed by signals according to a specific communicationprotocol. The proposed temporal transformation process is based on a set of formaltransformation rules. We have developed a tool performing the automatic refinement ofPSL specifications. As for design refinement assertion refinement is not fully automated.Temporal and structural information must be provided by the user, using an ergonomicinterface. The tool allows the generation of assertions in RTL but also hybrid assertions.Little work has been done before in this area, and the proposed solutions suffer from severerestrictions. To our knowledge, our prototype is the first tool that performs a temporaltransformation of assertions based on the formal semantics of a standard specificationlanguage (PSL).

This work aims at methods, which are suitable for mixed-signal integrated circuit verification. The emphasis is on the Assertion-based verification. In practice there are two languages, which can be used for this method - PSL and SystemVerilog. These languages are compared between each other and individually tested to find their capabilities, functional limits and restrictions. One of them will be integrated into verification flow of SCG Czech Design Center s. r. o. company to develop ABV methodology in analog and mixed-signal domain.

Au-delà de la formidable évolution en termes de complexité du circuit électronique en soi, son adoption et sa diffusion ont connu, au fil des dernières années, une explosion dans un très grand nombre de domaines distincts. Un système sur puce peut incorporer une combinaison de composants aux fonctionnalités très différentes. S'assurer du bon fonctionnement de chaque composant, et du système complet, est une tâche primordiale et épineuse. Dans ce contexte, l'Assertion-Based Verification (ABV) a considérablement gagné en popularité ces dernières années : il s'agit d'une démarche de vérification où des propriétés logico-temporelles, exprimées dans des langages tels que PSL ou SVA, spécifient le comportement attendu du design. Alors que la plupart des solutions d'ABV existantes se limitent au niveau transfert de registres (RTL), la contribution décrite dans cette thèse s'efforce de résoudre un certain nombre de limitations et vise ainsi une solution mature pour le niveau transactionnel (TLM) de SystemC. Une technique efficace de construction de moniteurs de surveillance à partir de propriétés PSL est proposée : cette technique, inspirée d'une approche originale existante pour le niveau RTL, est ici adaptée à SystemC TLM. Une méthode spécifique de surveillance des actions de communication à haut niveau d'abstraction est également détaillée. Les possibilités offertes par la technique présentée sont significativement étendues en proposant, pour les propriétés écrites en langage PSL, à la fois un support formel et une mise en oeuvre pratique pour des variables auxiliaires globales et locales, qui constituent un élément essentiel lors des spécifications à haut niveau d'abstraction. Tous ces concepts sont également implémentés dans un outil prototype. Afin d'illustrer l'intérêt de la solution proposée, diverses expérimentations sont effectuées avec des designs aux dimensions et complexités différentes. Les résultats obtenus permettent de souligner le fait que la méthode de vérification dynamique suggérée reste applicable pour des designs de taille réaliste. / Over the last years, the growing of electronic circuit complexity has experienced a tremendous evolution. Moreover, electronic circuits have become widespread elements in many different areas. This development leads to Systems-on-Chip incorporating a combination of components with highly heterogeneous features. Ensuring the correct behavior of each component, as well as validating the behavior of the whole system, is both a compelling and painful task. In this context, Assertion-Based Verification (ABV) has widely gained acceptance over the recent years : following this approach, temporal properties expressed using languages such as PSL or SVA specify the expected behavior of the design. While most existing ABV solutions are restricted to the register transfer level (RTL), the work of this thesis attempts to overcome some limitations by developing an actual ABV solution for the transaction level modeling (TLM) in SystemC. An effective technique for the construction of checker modules from PSL properties is proposed : this technique for SystemC TLM is inspired from a pioneering approach for RTL. A specific method for monitoring communication activities at a high level of abstraction is also described. The scope of the proposed technique is significantly improved by adding to PSL both a formal and a practical support for auxiliary global and local variables, which are compelling in higher level specifications. All these concepts are implemented in a prototype tool. In order to present the applicability of the proposed solution, we performed various experiments using designs of different sizes and complexities. The experimental results show that this dynamic verification methodology is also suitable for real-world designs.

Au-delà de la formidable évolution en termes de complexité du circuit électronique en soi, son adoption et sa diffusion ont connu, au fil des dernières années, une explosion dans un très grand nombre de domaines distincts. Un système sur puce peut incorporer une combinaison de composants aux fonctionnalités très différentes. S'assurer du bon fonctionnement de chaque composant, et du système complet, est une tâche primordiale et épineuse. Dans ce contexte, l'Assertion-Based Verification (ABV) a considérablement gagné en popularité ces dernières années : il s'agit d'une démarche de vérification où des propriétés logico-temporelles, exprimées dans des langages tels que PSL ou SVA, spécifient le comportement attendu du design. Alors que la plupart des solutions d'ABV existantes se limitent au niveau transfert de registres (RTL), la contribution décrite dans cette thèse s'efforce de résoudre un certain nombre de limitations et vise ainsi une solution mature pour le niveau transactionnel (TLM) de SystemC. Une technique efficace de construction de moniteurs de surveillance à partir de propriétés PSL est proposée : cette technique, inspirée d'une approche originale existante pour le niveau RTL, est ici adaptée à SystemC TLM. Une méthode spécifique de surveillance des actions de communication à haut niveau d'abstraction est également détaillée. Les possibilités offertes par la technique présentée sont significativement étendues en proposant, pour les propriétés écrites en langage PSL, à la fois un support formel et une mise en oeuvre pratique pour des variables auxiliaires globales et locales, qui constituent un élément essentiel lors des spécifications à haut niveau d'abstraction. Tous ces concepts sont également implémentés dans un outil prototype. Afin d'illustrer l'intérêt de la solution proposée, diverses expérimentations sont effectuées avec des designs aux dimensions et complexités différentes. Les résultats obtenus permettent de souligner le fait que la méthode de vérification dynamique suggérée reste applicable pour des designs de taille réaliste.

Les travaux présentés dans cette thèse portent sur la modélisation, la spécification et la vérification des modèlesdes Systèmes sur Puce (SoCs) au niveau d’abstraction transactionnel et à un niveau d’abstraction plus élevé.Les SoCs sont hétérogènes: ils comprennent des composants matériels et des processeurs pour réaliser le logicielincorporé, qui est en lien direct avec du matériel. La modélisation transactionnelle (TLM) basée sur SystemCa été très fructueuse à fournir des modèles exécutables des SoCs à un haut niveau d’abstraction, aussi appelésprototypes virtuels (VPs). Ces modèles peuvent être utilisés plus tôt dans le cycle de développement des logiciels,et la validation des matériels réels. La vérification basée sur assertions (ABV) permet de vérifier les propriétés tôtdans le cycle de conception de façon à trouver les défauts et faire gagner du temps et de l’effort nécessaires pourla correction de ces défauts. Les modèles TL peuvent être sur-contraints, c’est-à-dire qu’ils ne presentent pastous les comportements du matériel. Ainsi, ceci ne permet pas la détection de tous les défauts de la conception.Nos contributions consistent en deux parties orthogonales et complémentaires: D’une part, nous identifions lessources des sur-contraintes dans les modèles TLM, qui apparaissent à cause de l’ordre d’interaction entre lescomposants. Nous proposons une notion d’ordre mou qui permet la suppression de ces sur-contraintes. D’autrepart, nous présentons un mécanisme généralisé de stubbing qui permet la simulation précoce avec des prototypesvirtuels SystemC/TLM.Nous offrons un jeu de patrons pour capturer les propriétés d’ordre mou et définissons une transformationdirecte de ces patrons en moniteurs SystemC. Notre mécanisme généralisé du stubbing permet la simulationprécoce avec les prototypes virtuels SystemC/TLM, dans lesquels certains composants ne sont pas entièrementdéterminés sur les valeurs des données échangées, l’ordre d’interaction et/ou le timing. Ces composants nepossèdent qu’une spécification abstraite, sous forme de contraintes entre les entrées et les sorties. Nous montronsque les problèmes essentielles de la synchronisation entre les composants peuvent être capturés à l’aide de notresimulation avec les stubs. Le mécanisme est générique; nous mettons l’accent uniquement sur les concepts-clés,les principes et les règles qui rendent le mécanisme de stubbing implémentable et applicable aux études de casindustriels. N’importe quel language de spécification satisfaisant nos exigences (par ex. le langage des ordresmou) peut être utilisé pour spécifier les composants, c’est-à-dire il peut être branché au framework de stubbing.Nous fournissons une preuve de concept pour démontrer l’intérêt d’utiliser la simulation avec stubs pour ladétection anticipée et la localisation des défauts de synchronisation du modèle. / The work presented in this thesis deals with modeling, specification and testing of models of Systems-on-a-Chip (SoCs) at the transaction abstraction level and higher. SoCs are heterogeneous: they comprise bothhardware components and processors to execute embedded software, which closely interacts with hardware.SystemC-based Transaction Level Modeling (TLM) has been very successful in providing high-level executablecomponent-based models for SoCs, also called virtual prototypes (VPs). These models can be used early in thedesign flow for the development of the software and the validation of the actual hardware. For SystemC/TLMvirtual prototypes, Assertion-Based Verification (ABV) allows property checking early in the design cycle,helping to find bugs early in the model and to save time and effort that are needed for their fixing. TL modelscan be over-constrained, which means that they do not represent all the behaviors of the hardware, and thus,do not allow detection of some malfunctions of the prototype. Our contributions consist of two orthogonal andcomplementary parts: On the one hand, we identify sources of over-constraints in TL models appearing due tothe order of interactions between components, and propose a notion of loose-ordering which allows to removethese over-constraints. On the other hand, we propose a generalized stubbing mechanism which allows the veryearly simulation with SystemC/TLM virtual prototypes.We propose a set of patterns to capture loose-ordering properties, and define a direct translation of thesepatterns into SystemC monitors. Our generalized stubbing mechanism enables the early simulation with Sys-temC/TLM virtual prototypes, in which some components are not entirely determined on the values of theexchanged data, the order of the interactions and/or the timing. Those components have very abstract speci-fications only, in the form of constraints between inputs and outputs. We show that essential synchronizationproblems between components can be captured using our simulation with stubs. The mechanism is generic;we focus only on key concepts, principles and rules which make the stubbing mechanism implementable andapplicable for real, industrial case studies. Any specification language satisfying our requirements (e.g., loose-orderings) can be used to specify the components, i.e., it can be plugged in the stubbing framework. We providea proof of concept to demonstrate the interest of using the simulation with stubs for very early detection andlocalization of synchronization bugs of the design.

[pt] Diante da complexidade do ambiente de negócios contemporâneo e tendo em vista as limitações da racionalidade humana, os estudos da teoria do comportamento organizacional propostos e a teoria da visão baseada na atenção, este estudo objetiva diagnosticar o nível de atenção a temas críticos para a proteção empresarial e verificar a percepção sobre o nível de risco de situações propostas, por meio de pesquisa aplicada a profissionais que desempenham função gratificada em uma organização do setor de óleo e gás. Para tanto, com base em estudos desenvolvidos de atenção e percepção de risco, foi realizada pesquisa quantitativa de natureza descritiva, respondida voluntariamente por 409 profissionais ocupantes de função gratificada de diferentes áreas da empresa: de negócios e corporativas, de diferentes níveis organizacionais, níveis de formação, tempo de empresa e idade. Os resultados apontam que os temas relacionados à logística de produtos e pessoas são os assuntos com maior engajamento na captação da atenção, análise dos riscos relacionados e sobre os quais os profissionais participantes desta pesquisa investem mais tempo e esforço na busca de mais informações/conhecimentos. / [en] Given the complexity of the contemporary business environment and considering the limitations of human rationality, the proposed studies of the organizational behavior theory and the vision based in attention theory, this study aims to diagnose the level of attention to critical issues for corporate security and verify and the perception of the risk level of proposed situations, through research applied to professionals who perform a gratified position in an organization in the oil and gas sector. Therefore, based on studies developed on attention and risk perception, a quantitative descriptive research was carried out, answered voluntarily by 409 professionals occupying a gratified position in different areas on the company: business and the corporate, from different organizational levels, education level, time in the organization and age. The results show that topics related to the topics of products and people are the subjects with the greatest engagement in attracting attention, analyzing the related risks and on which the professionals participating in this research invest more time and the search for more information/knowledge.

L'objectif de cette thèse est d'étudier un système modélisant l'évolution d'écoulements bi-fluides non miscibles dans un domaine borné, avec la perspective de mieux comprendre et de prédire le comportement de bulles dans les c{\oe}urs de réacteurs nucléaires. Ce système, appelé DLMN, est construit à partir des équations de Navier-Stokes sous l'hypothèse d'un nombre de Mach très faible. Dans le cadre d'études préliminaires, on établit des résultats d'existence et d'unicité de solutions pour des données initiales régulières (de type Sobolev) et pour différents systèmes d'équations aux dérivées partielles non-linéaires couplant équations hyperboliques, paraboliques et elliptiques. En particulier, dans le cas du modèle abstrait de vibration de bulles (ABV), on établit un certain nombre de propriétés vérifiées par les solutions, lesquelles sont explicitées en dimension $1$. On s'attache ensuite à simuler ces solutions, en utilisant des schémas adaptés à la régularité des données. Pour le cas des données régulières, on construit un schéma d'ordre $2$ inconditionnellement stable et basé sur la méthode des caractéristiques. En revanche, en présence de discontinuités, on associe un schéma non diffusif à un algorithme de raffinement adaptatif de maillages.