L'être humain fait des erreurs, en particulier dans la réalisation de taches complexes comme la construction des systèmes informatiques modernes. Nous nous intéresserons dans cette thèse à la vérification assistée par ordinateur du bon fonctionnement des systèmes informatiques. Les systèmes informatiques actuels sont de grande complexité. Afin de garantir leur fiabilité, la vérification automatique est une alternative au 'testing' et à la simulation. Elle propose d'utiliser des ordinateurs pour explorer exhaustivement l'ensemble des états du système, ce qui est problématique: même des systèmes assez simples peuvent atteindre un grand nombre d'états. L'utilisation des bonnes représentations des espaces d'états est essentielle pour surmonter la complexité des problèmes posés en vérification automatique. La vérification des systèmes concurrents amène des difficultés additionnelles, car l'analyse doit, en principe, examiner tous les ordres possibles d'exécution des actions concurrentes. Le dépliage des réseaux de Petri est une technique largement étudiée pour la vérification des systèmes concurrents. Il représentent l'espace d'états du système par un ordre partiel, ce qui se révèle aussi naturel qu'efficace pour la vérification automatique. Nous nous intéressons à la vérification des systèmes concurrents modélisés par des réseaux de Petri, en étudiant deux techniques remarquables de vérification: le 'model checking' et le diagnostic. Nous étudions les dépliages des réseaux de Petri étendus avec des arcs de lecture. Ces dépliages, aussi appelés dépliages contextuels, semblent être une meilleure représentation des systèmes contenant des actions concurrentes qui lisent des ressources partagées : ils peuvent être exponentiellement plus compacts dans ces cas. Ce travail contient des contributions théoriques et pratiques. Dans un premier temps, nous étudions la construction des dépliages contextuels, en proposant des algorithmes et des structures de données pour leur construction efficace. Nous combinons les dépliages contextuels avec les 'merged process', une autre représentation des systèmes concurrents qui contourne l'explosion d'états dérivée du non-déterminisme. Cette nouvelle structure, appelée 'contextual merged process', est souvent exponentiellement plus compacte, ce que nous montrons expérimentalement. Ensuite, nous nous intéressons à la vérification à l'aide des dépliages contextuels. Nous traduisons vers SAT le problème d'atteignabilité des dépliages contextuels, en abordant les problèmes issus des cycles de conflit asymétrique. Nous introduisons également une méthode de diagnostic avec des hypothèses d'équité, cette fois pour des dépliages ordinaires. Enfin, nous implémentons ces algorithmes dans le but de produire un outil de vérification compétitif et robuste. L'évaluation de nos méthodes sur un ensemble d'exemples standards, et leur comparaison avec des techniques issues des dépliages ordinaires, montrent que la vérification avec des dépliages contextuels est plus efficace que les techniques existantes dans de nombreux cas. Ceci suggère que les dépliages contextuels, et les structures d'évènements asymétriques en général, méritent une place légitime dans la recherche en concurrence, également du point de vu de leur efficacité. / Humans make mistakes, especially when faced to complex tasks, such as the construction of modern hardware or software. This thesis focuses on machine-assisted techniques to guarantee that computers behave correctly. Modern computer systems are large and complex. Automated formal verification stands as an alternative to testing or simulation to ensuring their reliability. It essentially proposes to employ computers to exhaustively check the system behavior. Unfortunately, automated verification suffers from the state-space explosion problem: even relatively small systems can reach a huge number of states. Using the right representation for the system behavior seems to be a key step to tackle the inherent complexity of the problems that automated verification solves. The verification of concurrent systems poses additional issues, as their analysis requires to evaluate, conceptually, all possible execution orders of their concurrent actions. Petri net unfoldings are a well-established verification technique for concurrent systems. They represent behavior by partial orders, which not only is natural but also efficient for automatic verification. This dissertation focuses on the verification of concurrent systems, employing Petri nets to formalize them, and studies two prominent verification techniques: model checking and fault diagnosis. We investigate the unfoldings of Petri nets extended with read arcs. The unfoldings of these so-called contextual nets seem to be a better representation for systems exhibiting concurrent read access to shared resources: they can be exponentially smaller than conventional unfoldings on these cases. Theoretical and practical contributions are made. We first study the construction of contextual unfoldings, introducing algorithms and data structures that enable their efficient computation. We integrate contextual unfoldings with merged processes, another representation of concurrent behavior that alleviates the explosion caused by non-determinism. The resulting structure, called contextual merged processes, is often orders of magnitude smaller than unfoldings, as we experimentally demonstrate. Next, we develop verification techniques based on unfoldings. We define SAT encodings for the reachability problem in contextual unfoldings, thus solving the problem of detecting cycles of asymmetric conflict. Also, an unfolding-based decision procedure for fault diagnosis under fairness constraints is presented, in this case only for conventional unfoldings. Finally, we implement our verification algorithms, aiming at producing a competitive model checker intended to handle realistic benchmarks. We subsequently evaluate our methods over a standard set of benchmarks and compare them with existing unfolding-based techniques. The experiments demonstrate that reachability checking based on contextual unfoldings outperforms existing techniques on a wide number of cases. This suggests that contextual unfoldings, and asymmetric event structures in general, have a rightful place in research on concurrency, also from an efficiency point of view.

A busca por novas tecnologias de produção de flores e plantas ornamentais em ambiente protegido, que resultem no aumento da eficiência do uso da estrutura produtiva com incremento de produção e da qualidade, evolui constantemente. Esse estudo teve como objetivo analisar os efeitos dos diferentes telados de sombreamento (30%) vermelho e azul sobre o cultivo de três variedades de Lisianthus (Eustoma grandiflorum), variedade de flor rosa (Flare Deep Rosa), flor branca (Allemande White Bl) e de flor roxa (Echo Blue Bl), em relação ao crescimento da planta, desenvolvimento da cultura, coloração e pigmentação de folhas e pétalas. O tratamento controle, denominado telado controle foi conduzido sob cobertura de plástico transparente comum em produções comerciais. Com os resultados analisados estatisticamente, o telado vermelho obteve melhores resultados, com diferença significativa dos demais telados, para altura de plantas, comprimento de par de folha (expansão foliar), maiores teores de clorofila a e b, clorofila total e carotenoides, o telado controle se destacou por plantas com maiores teores de antocianina nas pétalas e o telado azul, com diferença signicativa dos demais, com piores resultados para concentrações de carotenoides, massa de haste colhida, número médio de botões por haste, menor diâmetro de haste ao longo do cultivo e na colheita, menor comprimento de par de folha e quanto a colheita que em comparação aos demais tratamentos esteve atrasada em 10 dias. / The search for new technologies for flower and ornamental plants production in greenhouses that result in increased efficiency of the productive structure use, to increase production and quality is constantly evolving. This study aimed to analyze the effects of different shading nets (30%) red and blue on the cultivation of three varieties of Lisianthus (Eustoma grandiflorum), variety of rose flower (Flare Deep Rose), white flower (Allemande White Bl) and purple flower (Echo Blue Bl) regarding to plant growth, development of culture and coloring and pigmentation of leaves and petals. The control treatment, called net control was conducted under a common transparent plastic cover used in commercial productions. The results of the statistical analysis demonstrated that, red net had better results, with significant difference between the other treatments, for plant height, lenght of pair of leaves (leaf expansion), higher content of chlorophyll a and b, total chlorophyll and carotenoids, net control is highlighted by plants with higher levels of anthocyanins in the petals and blue net, with signficant difference from the others, with worse results for carotenoids concentrations, stem weight, average number of buds per stem, thinner rod along the cultivation and harvesting, the lower length of pair of leaves and harvest as compared to other treatments was delayed by 10 days.

Este trabalho introduz a formalização algébrica do F-MFG (Functional Mark Flow Graph) para a análise e simulação computacional de modelos de sistemas antropocêntricos de produção, onde são enfocadas a interação e a interface do elemento humano com o sistema produtivo. Abordando os sistemas antropocêntricos como uma classe de sistemas a eventos discretos, o F-MFG, que é uma técnica baseada nas redes de Petri, comprova ter potencial para descrever detalhadamente as ações e estados do sistema. O F-MFG, em conjunto com a Metodologia PFS/MFG (Production Flow Schema/ Mark Flow Graph), estabelece um procedimento eficiente para o projeto de sistemas antropocêntricos, tornando concisa a modelagem e a posterior avaliação estrutural e comportamental do sistema. / This work introduces an algebraic formalization of F-MFG (Functional-Mark Flow Graph). This formalization is effective for analysis and simulation of anthropocentric production systems, which is focused on the interaction and interface between human elements and production systems. When approaching anthropocentric systems as Discrete Event Dynamic Systems, the F-MFG, which is a Petri Net based technique, has been demonstrated its potential capabilities in describing detailed models of system actions and states. The PFS/MFG Methodology (Production Flow Schema/Mark Flow Graph Methodology) combined with F-MFG establishes an efficient procedure for the design of anthropocentric systems. This procedure results in concise modeling and analysis (system structural and behavioral evaluation) processes.

Neste trabalho apresenta-se um estudo do comportamento estrutural de cestas protendidas, tendo em vista a sua utilização em coberturas pênseis de grandes áreas livres. A partir da Técnica do Meio Contínuo obtêm-se as equações que permitem analisar as cestas protendidas quanto a esforços e deslocamentos. Fazem-se considerações sobre o sistema de equações encontrado visando a sua resolução mediante o emprego de programa computacional como instrumento de cálculo. Apresentam-se exemplos numéricos e os resultados são comparados com os obtidos em outros trabalhos. Fazem-se algumas considerações a respeito do projeto e do cálculo de cestas protendidas, além de algumas indicações sobre a continuidade da pesquisa. / This work presents a continuous medium method analysis of cable nets and their applications as suspended roofs for large free spans. lnitially the theory of the method is presented and later applied to get the system of differential equation that represents the problem. Finally this system is numerically solved with computational procedures. Some examples are presented and the results compared with those obtained with others methods and numerical procedures. Some analysis and design considerations and further developments in this subject are also included.

O objetivo deste trabalho é o estudo dos processos informados de automação, isto é, onde o fluxo e armazenagem de informação são determinantes para o processo de negócio (PN), além de servir para verificação de qualidade, recuperação de erros, rastreabilidade de ocorrências anômalas, etc. Aborda-se em especial um tratamento onde a internacionalização do acesso aos dados (sistema EPCIS) passa por um elemento de captura e distribuição local, chamado SAVANT-2, que acaba por ser o elemento chave para controle do fluxo e para o desenvolvimento dos projetos (Dos Santos, 2005). As informações são capturadas por leitores de RFID, e não em código de barras como é feito convencionalmente. As etiquetas de código de barras geraram uma revolução nos sistemas de identificação há algumas décadas atrás, mas hoje se mostram inadequadas num número crescente de casos. O código de barras pode ser extremamente barato, mas tem baixa produtividade além de baixa capacidade de armazenamento de dados e uma dependência maior das operações manuais, quando comparado a outras tecnologias de suporte de dados. Um estudo de caso será feito na automação de acervos, onde a informação de base é a retirada e a devolução de obras por usuários, que é atualizada dinamicamente e está intimamente ligada à missão do próprio sistema de controle do acervo. Esse trabalho segue a mesma abordagem proposta por (Tavares, 2006) e (Dos Santos, 2005), ou seja, controlar a informação corporativa localmente e selecionar, além do código de identificação, as informações que podem e devem ser estrategicamente compartilhadas com o restante do mundo. Em outras palavras utilizaremos a modelagem do fluxo de informação em Redes de Petri e os sistemas denominados de SAVANT-2 e EPCIS-2.Para isso, foram desenvolvidos novos módulos EPCIS-2 e SAVANT-2 adaptados dos já desenvolvidos, só que acoplados a leitores e sensores, que compõe um piloto simplificado de um sistema de controle para biblioteca. Este protótipo instalado no Design Lab da Escola Politécnica da Universidade de São Paulo gerencia o acervo de livros e mídias do laboratório. Este é não somente o 1º acervo da América Latina automatizado com sistema utilizando a tecnologia RFID, mas também o primeiro automatizado com base na Rede EPC e com a análise de eventos atípicos de seus processos no mundo. / The objective of this work is to study the informed automation processes, in which the information flow and storage are essential to the business process, providing quality control, error recovering, traceability and the track of anomalous occurrences. In such processes the capture of the proper pieces of information is a key point to the automation process, observing the mission assigned to the system. We focus on a case-study of a heap library service, treating the information with RFID (Radio Frequency Identification), reusing the intermediary system SAVANT-2 (Dos Santos, 2005) and a database to the target storage. Barcode labels caused a revolution in the identification systems a few decades ago, but have become inadequate in an increasing number of cases. Barcodes can be extremely inexpensive, but it has low productivity and low data storage capacity. Moreover, it depends more on manual operation, when compared to other technologies. This work follows the line so study of informed automation concepts explored in the work of (Tavares, 2006) and (Dos Santos, 2005) in a manufacturing application. In other words, the control of the corporate information, besides the identification code, is done locally and afterwards, strategic information is selected to be shared with the rest of the world. We use the dataflow modeling in Petri Nets and systems named SAVANT-2 and EPCIS-2. In order to support this work, new modules EPCIS-2 and SAVANT-2, proposed by (Tavares, 2006) and (Dos Santos, 2005) are expanded e implemented, adapting the existing ones to readers and sensors. A simplified project will be implemented in the Design Lab of the Escola Politécnica, Universidade de São Paulo (USP). This is not only the first catalog in the Latin America automated with an RFID system, but also the first in the world with automation based on EPC Networks and with atypical events analysis of its processes.

A segurança do espaço aéreo pode aumentar consideravelmente com o uso de operações de espaçamento e separação aerotransportados. Sob este paradigma, a tarefa de manter distância em relação a outras aeronaves é delegada aos pilotos, que contarão com o Sistema de Assistência de Separação Aerotransportado (ASAS). Com este sistema, ainda em fase experimental, os pilotos tornam-se cientes dos riscos do tráfego circundante com até 15 minutos de antecedência, sem necessitar de auxílio dos controladores de tráfego aéreo. Esta antecedência é muito maior que a do atual sistema anti-colisão (TCAS), que é de menos de 1 minuto. O sistema ASAS utiliza uma tecnologia de comunicação mais avançada que a tecnologia do transponder modo C, utilizado atualmente pelo sistema anti-colisão. O novo sistema ASAS está sendo desenvolvido intensivamente no Eurocontrol e em outras iniciativas nos Estados Unidos da América, e funcionará em conjunto com o atual sistema anti-colisão, proporcionando redundância, ou seja: se o antigo sistema falhar, o novo ainda pode emitir um alerta, ou vice-versa. O presente trabalho de pesquisa aborda a aplicação do ASAS para aumentar a precisão do espaçamento entre aeronaves que chegam sequencialmente a um determinado aeroporto, por meio de um formalismo matemático denominado \"Rede de Petri Estocástica e Dinamicamente Colorida\", com a obtenção de dados quantitativos sobre o risco de acidente. Esses dados indicam que o risco de acidente é significativamente menor com o uso do ASAS do que sem o uso do ASAS. / The safety in the airspace can considerably increase with the use of airborne spacing and separation operations. Under this paradigm, the task of maintaining a safe distance between aircraft is delegated to the pilots, which will be supported by the Airborne Separation Assistance System (ASAS). With this system, which is still in experimental phase, pilots become aware of the surrounding air traffic risks with up to 15 minutes in advance, without the help of air traffic controllers on the ground. This antecedence is much greater than the one provided by the current Traffic Collision Avoidance System (TCAS). ASAS uses a more advanced communication technology than Mode-C transponder, broadly used in the current civil aviation for collision avoidance purposes. The development of ASAS is being carried out intensively in Eurocontrol and in other initiatives in the United States of America, and this novel system is intended to work in parallel with the current collision avoidance systems, acting as safety nets. The present study approaches the ASAS application to improve the precision of spacing between aircraft that sequentially arrive at an airport, using the so called mathematical formalism \"Stochastically and Dynamically Coloured Petri Net\", for evaluating quantitative data about accident risk. These data indicate that the accident risk is significantly smaller when aircraft pairs use ASAS Spacing than when aircraft pairs do not use ASAS Spacing.

Propõe-se uma estratégia de modelagem e de análise formal de políticas de segurança para sistemas baseados em fluxos de trabalho (workflows) e contendo regras que envolvam aspectos de lógica de negócios. Verifica-se com o auxílio de uma política de exemplo que a estratégia proposta resulta em modelos amplamente capazes de expressar restrições lógicas em função de parâmetros de negócio sem comprometer a viabilidade de suas análises. A modelagem baseia-se no uso de um metamodelo definido a partir da identificação das entidades que caracterizam o estado de proteção de um sistema e representado na forma de uma rede de Petri colorida. Por meio da escrita de predicados para consulta sobre o espaço de estados da rede de Petri, verifica-se o atendimento às regras de segurança no modelo formal. A tratabilidade da análise é garantida pela adoção de um paradigma diferenciado principalmente pela busca de ramos inseguros em vez de nós inseguros no espaço de estados e por explorar a natureza independente entre serviços de negócio distintos, expressa por restrições ao fluxo de informação no metamodelo. Tais restrições permitem que a análise seja fracionada evitando o problema da explosão de estados. O exemplo discutido de modelagem e análise de um sistema de serviços bancários online fornece evidências suficientes para atestar a aplicabilidade do método à validação de políticas de segurança para sistemas reais. / A strategy is proposed for the formal modeling and analysis of workflow- -based security policies having rules which involve aspects of business logic. Aided by an example of security policy, the proposed strategy is shown to lead to models widely capable of expressing logical restrictions as functions of business parameters without compromising the feasibility of its analyses. The modeling is based on the usage of a metamodel defined from the identification of the entities that characterize the protection state of a system, and represented as a colored Petri net. By writing predicates for querying the Petri net state-space, compliance with security rules at the formal model is verified. The feasibility of the analysis is ensured by the adoption of a paradigm distinguished mainly for the search for insecure branches rather than insecure nodes in the state-space, and for exploiting the independent nature among different business services, expressed by restrictions to the information flow within the metamodel. Such restrictions allow the analysis to be fractioned, avoiding the state explosion problem. The example provided of modeling and analysis of an online banking services system offers enough evidence to attest the applicability of the method to the validation of security policies for real-world systems.

As importantes transformações das organizações nos últimos anos mostram que diferentes princípios de qualidade, competitividade e inovação devem ser conjugados para o projeto de sistemas de controle de sistemas produtivos. Esta abordagem, que traz benefícios às organizações, é viável em virtude da evolução das estratégias de integração e da tecnologia da informação. A partir da norma em elaboração ANSI/ISA S95, esta dissertação desenvolve procedimentos para definição do escopo funcional, requisitos e modelagem para o projeto de sistemas de controle de sistemas produtivos integrados à organização, atuando de forma estruturada, em conformidade com padrões técnicos de automação e engenharia de requisitos. Como resultados, estabelece procedimentos para o início do projeto que definem o escopo funcional do sistema de controle de sistemas produtivos integrado à gestão da organização. A seguir, estes procedimentos estabelecem os domínios semânticos dos subsistemas necessários para o desempenho de suas funções, acompanhados das respectivas linguagens de modelagem. A dissertação completa-se com a modelagem dos subsistemas através do E-MFG com comunicadores, modelagem esta que suporta os padrões existentes de programação da automação. Neste contexto, parte-se dos requisitos de cada subsistema coletados por uma versão modificada do caso de uso da UML, convertidos finalmente para o E-MFG com comunicadores. / The important changes that are happening inside organizations show that different principles of quality, innovation and competition should be combined during the design of control system of production systems. This approach is possible thanks to the evolution of integration strategy and information technology, generating benefits to organizations. Procedures are established to define system’s functional scope, requirements and models, based on the integrated approach of ANSI/ISA S95 standard. The procedures are developed by a structured process and according to automation standards and requirements engineering. The work’s first result is a procedure that defines a functional scope for control system design of production systems integrated with organization. As a second result, procedures help to define semantic domains of all subsystems needed to develop control system functions, as well as the modeling techniques for each domain. The result is complemented by modeling subsystems using an extended version of Mark Flow Graph (E-MFG with communicators). This task has the assistance of a modified use case version from “Unified Modeling Language” to collect requirements before modeling.

Submitted by admin tede (tede@pucgoias.edu.br) on 2018-11-08T18:17:38Z No. of bitstreams: 1 JULIANO RESENDE BUCCHIANDERI.pdf: 6086819 bytes, checksum: ec188a1a0edcce38757a6e0f604df66d (MD5) / Made available in DSpace on 2018-11-08T18:17:38Z (GMT). No. of bitstreams: 1 JULIANO RESENDE BUCCHIANDERI.pdf: 6086819 bytes, checksum: ec188a1a0edcce38757a6e0f604df66d (MD5) Previous issue date: 2018-09-11 / The appropriated and secure supply of electrical energy directly impacts on the present society. The increase in demand favors the growth of electrical systems, especially in distribution networks and substations, since they are responsible for lowering the electrical voltage, allowing energy distribution to the population. To keep distribution networks and substations running, without interruption or discontinuity, is utmost importance for the maintenance of electric power supply, and it is necessary to implement means to locate and improve the electrical protections in order to reduce failures or to suspend the electricity distribution. Distribution failures may result from lightning, overcurrent, short circuits, overvoltages, oil leakage on transformers, impedance failure etc. The present work presents the problem of possible defects that result in the substation power blackout, and aims to reduce the amount and frequency of substation power blackouts, contributing to the increase in industrial production. In this regard, qualitative and quantitative models using Petri nets of an electrical substation of distribution were developed, using simulation scenarios to indicate possible improvements in the electrical protections, reducing the inaccuracies and interruptions. / O fornecimento adequado e seguro de energia elétrica impacta diretamente na sociedade atual. O aumento da demanda torna favorável o crescimento dos sistemas de eletricidade, sobretudo nas redes e subestações de distribuição, pois estas são responsáveis por rebaixar a tensão elétrica, permitindo assim distribuição de energia para a população. Manter as redes e subestações de distribuição funcionando, sem interrupções ou descontinuidade, é de suma importância para a manutenção do fornecimento de eletricidade, sendo necessário implementar meios para localizar e melhorar as proteções elétricas afim de diminuir as falhas ou a suspensão da distribuição desta. As falhas da distribuição podem resultar de descargas atmosféricas, sobrecorrente, curtoscircuitos, sobretensões, vazamento de óleo nos transformadores, falha de impedância etc. O presente trabalho expõe o problema dos possíveis defeitos que resultam no desligamento da subestação e objetiva reduzir a quantidade e a frequência dos desligamentos da subestação, colaborando para o aumento na produção industrial. Para isso, desenvolveu modelos qualitativos e quantitativos utilizando redes de Petri de uma subestação elétrica de distribuição, utilizando cenários de simulação para apontar possíveis melhorias nas proteções diminuindo as incorreções e interrupções.

Submitted by Jorge Silva (jorgelmsilva@ufrrj.br) on 2018-11-12T20:44:46Z No. of bitstreams: 1 2018 - Tatiane Lima da Silva.pdf: 3356978 bytes, checksum: 814f934a7b82c576f5248ee783fb8c66 (MD5) / Made available in DSpace on 2018-11-12T20:44:46Z (GMT). No. of bitstreams: 1 2018 - Tatiane Lima da Silva.pdf: 3356978 bytes, checksum: 814f934a7b82c576f5248ee783fb8c66 (MD5) Previous issue date: 2018-03-02 / CAPES / The Atlantic Rainforest is currently one of the most threatened biomes, considered global priority of conservation. Most of its forest remnants are in the form of small fragments. Forest fragmentation processes can lead to negative consequences for avifauna, such as the loss of specialized species, and increase in the proportion of opportunistic species. This study aimed to survey birds in forest fragments located in three private properties: Ip? Grange (IG), Monumento Grange (MG) and Fortaleza Farm (FF), located in Cacaria, Pira?, RJ. In the first chapter, a comparison was performed for the bird communities of the three sites regarding richness, frequency of occurrence, composition, abundance, diversity, equability and trophic guilds. In the second chapter, the biology of birds captured in mist networks in terms of capture and effort rate, seasonality, morphometric variation, body mass, feather molting and incubation plate were analyzed. The mist nets survey was conducted between August 2015 and February 2017, in which ten mist nets were opened from 06:00 a.m. to 17:00 p.m. Eight, eleven and nine field days were dispensed in SI, SM and FF, respectively. Four points counts were sampled in each fragment monthly between May 2016 and April 2017. A total of 205 species were recorded, with FF displaying the highest richness (147 sp) and the second highest diversity (H' = 4.38), MG displayed the second highest richness (130 sp) and the highest diversity (H' = 4.42), followed by IG, with the lowest wealth (122 sp) and diversity (H' = 4.26). Species composition varied significantly among the three sampled areas (F = 5,15; p = 0,0002), with each site presenting a different composition in relation to the others. A predominance of insectivorous and omnivorous species was observed in the three fragments. A total of 252 individuals were captured, distributed between 77 bird species. The dry season presented a higher catch rate (10.5%) when compared to the rainy season (6.6%), revealing a seasonal pattern. The highest body mass was observed for Leptotila rufaxilla (187.4g ? 16.72; n = 7,) and the lowest for Hylocharis cyanus (0.6g; n = 1). Beak length and total length presented the highest and the lowest coefficient of variation, respectively. When analyzing morphometric variations between sexes, in Manacus manacus, only wing, tail and tarsal length were significantly different. Of the total number of captured individuals, 71 (28.3%) displayed a brood patch and 37 (14.6%) were molting. The brood patch and molting were associated with season (?2 = 20.627; p = 0.000005 and ?2 = 8.363; p = 0.0038, respectively). In 16 individuals (6.34%), a molt and brood patch overlap was found, with molt associated with the brood patch (?2 = 4.408; p = 0.035). Although the study area was represented by small forest fragments with a certain degree of environmental impact, a significant local diversity was found, with the presence of endemic and endangered species. / A Mata Atl?ntica ? um dos biomas mais amea?ados atualmente e considerada como prioridade mundial de conserva??o. A maior parte de seus remanescentes florestais encontra-se na forma de pequenos fragmentos. O processo de fragmenta??o florestal pode trazer consequ?ncias negativas para a avifauna, como a perda de esp?cies especializadas e aumento de esp?cies oportunistas. Este trabalho teve como objetivo o levantamento de aves em fragmentos florestais localizados em tr?s propriedades particulares: o S?tio Ip? (SI), o S?tio Monumento (SM) e a Fazenda Fortaleza (FF), situados em Cacaria, Pira?, RJ. No primeiro cap?tulo foi realizado uma compara??o da comunidade de aves entre estes tr?s locais quanto a riqueza, frequ?ncia de ocorr?ncia, composi??o, abund?ncia, diversidade, equabilidade e guildas tr?ficas. No segundo cap?tulo, foram analisados aspectos da biologia das aves capturadas em redes de neblina quanto a taxa e esfor?o de captura, sazonalidade, varia??o morfom?trica, massa corporal, muda de penas e placa de incuba??o. O levantamento por redes foi realizado entre agosto/2015 a fevereiro/2017, na qual dez redes de neblina foram abertas das 06:00h ?s 17:00h. Foram dispensados oito, 11 e nove dias em campo no SI, SM e FF, repectivamente. Quatro pontos de escuta foram amostrados em cada fragmento mesalmente, entre maio/ 2016 a abril/2017. Foram registradas 205 esp?cies, na qual a FF foi local com a maior riqueza (147 sp) e a segunda maior diversidade (H?= 4,38). O SM apresentou a segunda maior riqueza (130 sp) e a maior diversidade (H?= 4,42). J? o SI demonstrou a menor riqueza (122 sp) e diversidade (H? = 4,26). A composi??o de esp?cies variou significativamente entre as tr?s ?reas amostradas (F = 5,15; p = 0,0002), na qual cada local apresentou uma composi??o diferente em rela??o aos demais. Houve predomin?ncia de esp?cies inset?voras e on?voras nos tr?s fragmentos. Foram capturados 252 indiv?duos distribu?dos em 77 esp?cies de aves. A esta??o seca apresentou maior taxa de captura (10,5%) quando comparada ? esta??o chuvosa (6,6%), revelando um padr?o sazonal. A maior massa corp?rea foi encontrada em Leptotila rufaxilla (187,4g ? 16,72; n = 7) e a menor em Hylocharis cyanus (0,6g; n = 1). O comprimento do bico e comprimento total apresentaram o maior e o menor coeficiente de varia??o, respectivamente. Na an?lise de varia??o morfom?trica entre sexos em Manacus manacus, apenas o comprimento da asa, da cauda e do tarso apresentaram diferen?as significativas. Do total de indiv?duos capturados, 71 (28,3%) apresentaram placa de incuba??o e 37 (14,6%) estavam com muda de penas. A placa de incuba??o e a muda foram associadas ? esta??o do ano (?2 = 20,627; p = 0,000005 e ?2 = 8,363; p = 0,0038, respectivamente). Em 16 indiv?duos (6,34%) foi encontrado sobreposi??o da muda e placa, estando a muda associada a placa de incuba??o (?2 = 4,408; p = 0,035). Apesar da ?rea de estudo ser representada por pequenos fragmentos florestais com um certo grau de impacto ambiental, foi encontrado uma significativa diversidade local, com a presen?a de esp?cies end?micas e amea?adas.