Made available in DSpace on 2014-12-17T15:47:43Z (GMT). No. of bitstreams: 1 SalernoFSS.pdf: 1043687 bytes, checksum: ea5c1000dc1ef3c9200e040e16a2da89 (MD5) Previous issue date: 2007-01-25 / With hardware and software technologies advance, it s also happenning modifications in the development models of computational systems. New methodologies for user interface specification are being created with user interface description languages (UIDL). The UIDLs are a way to have a precise description in a language with more abstraction and independent of how will be implemented. A great problem is that even using these nowadays methodologies, we still have a big distance between the UIDLs and its design, what means, the distance between abstract and concrete. The tool BRIDGE (Interface Design Generator Environment) was created with the intention of being a linking bridge between a specification language (the Interactive Message Modeling Language IMML) and its implementation in Java, linking the abstract (specification) to the concrete (implementation). IMML is a language based on models, that allows the designer works in distinct abstraction levels, being each model a distinct abstraction level. IMML is a XML language, that uses the Semiotic Engineering concepts, that deals the computational system, with the user interface and its elements like a metacommunicative artifact, where these elements must to transmit a message to the user about what task must to be realized and the way to reach this goal. With BRIDGE, we intend to supply a lot of support to the design task, being the user interface prototipation the greater of them. BRIDGE allows the design becomes easier and more intuitive coming from an interface specification language / Com o avan?o das tecnologias de hardware e software, tem havido, tamb?m, modifica??es nos modelos de desenvolvimento de sistemas computacionais. Novas metodologias para especifica??o de interfaces de usu?rio est?o sendo criadas usando linguagens de descri??o de interfaces de usu?rio (LDIU). As LDIUs s?o uma forma de se ter uma descri??o precisa numa linguagem mais abstrata e independente de como ser? a implementa??o. Um grande problema ? que mesmo utilizando essas metodologias vigentes, ainda temos uma grande dist?ncia entre as LDIUs e o seu design, ou seja, a dist?ncia entre o abstrato e o concreto. A ferramenta BRIDGE (Interface Design Generator Environment) foi criada com o intuito de ser uma ponte de liga??o entre uma linguagem de especifica??o (a Interactive Message Modeling Language IMML) e a sua implementa??o em Java, ligando o abstrato (especifica??o) ao concreto (implementa??o). A IMML ? uma linguagem baseada em modelos, o que permite ao designer trabalhar com diferentes n?veis de abstra??o, sendo cada modelo um n?vel de abstra??o diferente. A IMML ? uma linguagem XML que se utiliza dos conceitos da Engenharia Semi?tica, que trata o sistema computacional, com a interface de usu?rio e seus elementos como um artefato metacomunicativo, onde os mesmos devem passar uma mensagem ao usu?rio sobre qual a tarefa a ser realizada e a forma de se alcan?ar este objetivo. Com o BRIDGE, visamos fornecer diversas ajudas ? tarefa de design, sendo a prototipa??o de interfaces de usu?rio a principal delas. O BRIDGE permite que o design a partir de uma linguagem de especifica??o de interfaces fique mais f?cil, intuitivo e produtivo

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-06-23T19:59:24Z No. of bitstreams: 1 FernandaMariaDeOliveira_DISSERT.pdf: 5023454 bytes, checksum: ad313de2391d707658adc05fbcb2a8e0 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-06-27T19:42:35Z (GMT) No. of bitstreams: 1 FernandaMariaDeOliveira_DISSERT.pdf: 5023454 bytes, checksum: ad313de2391d707658adc05fbcb2a8e0 (MD5) / Made available in DSpace on 2016-06-27T19:42:35Z (GMT). No. of bitstreams: 1 FernandaMariaDeOliveira_DISSERT.pdf: 5023454 bytes, checksum: ad313de2391d707658adc05fbcb2a8e0 (MD5) Previous issue date: 2014-07-31 / No Brasil, o controle da qualidade do ?leo Diesel comercializado ? realizado por monitoramento de propriedades f?sico-qu?micas, caracter?sticas do combust?vel atrav?s das Resolu??es ANP n? 65 de 09 de dezembro de 2011 e n? 45 de 20 de dezembro de 2012, que determinam os limites de especifica??o para cada par?metro e as metodologias de an?lise que devem ser adotados. No entanto, esses m?todos, apesar de bastante consolidados, possuem alguns inconvenientes t?cnicos, que levaram ao estudo de m?todos alternativos mais r?pidos e de menor custo. Este trabalho realizou uma avalia??o da aplicabilidade de equa??es matem?ticas dispon?veis na literatura e de Redes Neurais Artificiais (RNAs), na determina??o de par?metros de especifica??o do ?leo diesel. Foi realizado um levantamento bibliogr?fico das principais correla??es adequadas para a determina??o de propriedades do diesel, as quais foram aplicadas para obten??o do ponto de fulgor e do ?ndice de cetano, al?m da aplica??o, de forma mais resumida, para predizer propriedades do petr?leo. Para este estudo, foram utilizadas 162 amostras de diesel, com teores m?ximo de enxofre, 50 ppm, 500 ppm e 1800 ppm, que foram analisadas, em laborat?rio especializado, por meio de metodologias ASTM normatizadas pela ANP, com um total de 810 ensaios. Resultados experimentais das amostras de diesel, destila??o atmosf?rica, ASTM D86, e massa espec?fica, ASTM D4052, foram utilizados como vari?veis b?sicas de entrada para as equa??es avaliadas. As RNAs foram avaliadas para a predi??o do ponto de fulgor, ?ndice de cetano e teores de enxofre (S50, S500, S1800) e, nesta parte do trabalho foram testados dois tipos de arquiteturas de rede, feed-forward backpropagation e generalized regression, variando os par?metros da matriz de entrada de forma a determinar o grupo de vari?veis e melhor tipo de rede para predi??o das vari?veis de interesse. Os resultados obtidos pelas equa??es e pelas RNAs foram comparados com resultados experimentais obtidos por metodologias padr?o, utilizando o teste n?o param?trico de Mann-Whitney e test t de student, ao n?vel de signific?ncia de 5%, assim como pelo coeficiente de determina??o e erro percentual. Os resultados obtidos pela equa??o aplicada para o ponto de fulgor apresentou um erro de 27, 6 %, contudo observou-se uma tend?ncia um tanto similar aos resultados padr?o. O ?ndice de cetano foi obtido por tr?s equa??es, e ambas apresentaram bons coeficientes de correla??o, com destaque para equa??o baseada no ponto de anilina, que apresentou o menor erro de 0,8 %. As equa??es aplicadas ao petr?leo foram trabalhadas de forma a identificar perspectivas de trabalhos futuros, que se mostram bastante promissores. As RNAs para predi??o do ponto de fulgor e do ?ndice de cetano mostraram resultados bastante superiores ao observados com as equa??es matem?ticas, com erros respectivamente de 2,5% e 0,2%. Para os teores de enxofre S50, S500, e S1800, as RNAs constru?das utilizando como dados de entrada a destila??o D86 (T10, T50, T85 e T90), Massa Espec?fica, ?ndice de Cetano e Ponto de Fulgor apresentaram os melhores resultados. Dentre os teores de enxofre as RNAs conseguiram melhor predizer o S1800, e o erro obtido a partir dos resultados das RNAs aumentou com a diminui??o do teor de enxofre. De um modo geral, as redes do tipo feed-forward mostraram-se superiores as generalized regression. / Diesel fuel is one of leading petroleum products marketed in Brazil, and has its quality monitored by specialized laboratories linked to the National Agency of Petroleum, Natural Gas and Biofuels - ANP. The main trial evaluating physicochemical properties of diesel are listed in the resolutions ANP N? 65 of December 9th, 2011 and N? 45 of December 20th, 2012 that determine the specification limits for each parameter and methodologies of analysis that should be adopted. However the methods used although quite consolidated, require dedicated equipment with high cost of acquisition and maintenance, as well as technical expertise for completion of these trials. Studies for development of more rapid alternative methods and lower cost have been the focus of many researchers. In this same perspective, this work conducted an assessment of the applicability of existing specialized literature on mathematical equations and artificial neural networks (ANN) for the determination of parameters of specification diesel fuel. 162 samples of diesel with a maximum sulfur content of 50, 500 and 1800 ppm, which were analyzed in a specialized laboratory using ASTM methods recommended by the ANP, with a total of 810 trials were used for this study. Experimental results atmospheric distillation (ASTM D86), and density (ASTM D4052) of diesel samples were used as basic input variables to the equations evaluated. The RNAs were applied to predict the flash point, cetane number and sulfur content (S50, S500, S1800), in which were tested network architectures feed-forward backpropagation and generalized regression varying the parameters of the matrix input in order to determine the set of variables and the best type of network for the prediction of variables of interest. The results obtained by the equations and RNAs were compared with experimental results using the nonparametric Wilcoxon test and Student's t test, at a significance level of 5%, as well as the coefficient of determination and percentage error, an error which was obtained 27, 61% for the flash point using a specific equation. The cetane number was obtained by three equations, and both showed good correlation coefficients, especially equation based on aniline point, with the lowest error of 0,816%. ANNs for predicting the flash point and the index cetane showed quite superior results to those observed with the mathematical equations, respectively, with errors of 2,55% and 0,23%. Among the samples with different sulfur contents, the RNAs were better able to predict the S1800 with error of 1,557%. Generally, networks of the type feedforward proved superior to generalized regression.

Made available in DSpace on 2014-12-17T15:47:55Z (GMT). No. of bitstreams: 1 StephennsonSLG_DISSERT.pdf: 4909051 bytes, checksum: 2a9f94a42d9fc75bb16a1ff239148437 (MD5) Previous issue date: 2011-08-16 / This paper presents a contribution to the international Verified Software Repository effort through the formal specification of the microkernel FreeRTOS real-time system. Such specification was made in abstract level making use of the B method . For thus, properties of the microkernel were chosen and selected as specification requisites, which was constructed centered at the functionalities responsible for the utilization of these properties. This properties weres setting as specification requirements. The specification was constructed modeling the function of microkernel that implement this properties. This work intended to encourage the formal verification of FreeRTOS and also contribute to the formal creation of a microkernel real-time systems, based in FreeRTOS. Furthermore, this model brings a formal documentation point view of the microkernel, demonstrating features and how this internal states is changing. Finally, this work could be an example of specification of the actual system by the B method. / Este trabalho apresenta uma contribui??o para o esfor?o internacional do Verified Software Repository atrav?s da especifica??o formal da biblioteca de sistema de tempo real FreeRTOS. Tal especifica??o foi realizada de forma abstrata utilizando o m?todo B. Para isso, propriedades disponibilizadas por essa biblioteca foram elencadas e selecionadas como requisitos da especifica??o, a qual foi constru?da centrada nas funcionalidades respons?veis pela utiliza??o dessas propriedades. Com a modelagem desenvolvida pretende-se incentivar a verifica??o formal do FreeRTOS e tamb?m contribuir para a cria??o formal de uma biblioteca de sistemas de tempo real baseada na FreeRTOS. Al?m disso, tal modelagem traz uma documenta??o do ponto de vista formal do sistema, demonstrando como ocorrer internamente o seu funcionamento e serve como um exemplo da especifica??o de um sistema real pelo m?todo B.

Made available in DSpace on 2014-12-17T14:55:39Z (GMT). No. of bitstreams: 1 HaulissonJBC.pdf: 4077011 bytes, checksum: fcba1ed8fcdc3b273e8994b6775327be (MD5) Previous issue date: 2009-09-03 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / This work presents simulation results of an identification platform compatible with the INPE Brazilian Data Collection System, modeled with SystemC-AMS. SystemC-AMS that is a library of C++ classes dedicated to the simulation of heterogeneous systems, offering a powerful resource to describe models in digital, analog and RF domains, as well as mechanical and optic. The designed model was divided in four parts. The first block takes into account the satellite s orbit, necessary to correctly model the propagation channel, including Doppler effect, attenuation and thermal noise. The identification block detects the satellite presence. It is composed by low noise amplifier, band pass filter, power detector and logic comparator. The controller block is responsible for enabling the RF transmitter when the presence of the satellite is detected. The controller was modeled as a Petri net, due to the asynchronous nature of the system. The fourth block is the RF transmitter unit, which performs the modulation of the information in BPSK ?60o. This block is composed by oscillator, mixer, adder and amplifier. The whole system was simulated simultaneously. The results are being used to specify system components and to elaborate testbenchs for design verification / Este trabalho apresenta resultados de simula??o de uma plataforma de identifica??o compat?vel com o Sistema de Coleta de Dados Brasileiro do INPE, modelado com SystemC-AMS. SystemC-AMS, que ? uma biblioteca de classes C++ dedicada ? simula??o de sistemas heterog?neos, oferece um recurso poderoso para descrever modelos nos dom?nios digital, anal?gico e de RF, bem como sistemas mec?nicos e ?ticos. O modelo projetado foi dividido em quatro partes. O primeiro bloco leva em considera??o a ?rbita do sat?lite, necess?rio para modelar corretamente o canal, inclui o efeito Doppler, a atenua??o e o ru?do t?rmico. O bloco identifica??o que detecta a presen?a de sat?lite ? composto por um amplificador de baixo ru?do, filtro passa-banda, detector de pot?ncia e um comparador l?gico. O bloco controlador ? respons?vel por habilitar o transmissor RF, quando a presen?a do sat?lite ? detectada. O controlador foi modelado por uma rede de Petri, devido ? natureza ass?ncrona do sistema. O quarto bloco ? o transmissor, que realiza a modula??o da informa??o em BPSK ?60o. Este bloco ? composto por oscilador, misturadores, somador e amplificador. Todo o sistema foi simulado simultaneamente. Os resultados ser?o utilizados para especificar componentes de sistema e para a elabora??o de banco de testes para a verifica??o do projeto

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-05-31T20:52:30Z No. of bitstreams: 1 BrunaSoaresLandeira_TESE.pdf: 8601965 bytes, checksum: a68be4513e6834f5aaf48800f8ea90d7 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-06-01T22:19:30Z (GMT) No. of bitstreams: 1 BrunaSoaresLandeira_TESE.pdf: 8601965 bytes, checksum: a68be4513e6834f5aaf48800f8ea90d7 (MD5) / Made available in DSpace on 2017-06-01T22:19:30Z (GMT). No. of bitstreams: 1 BrunaSoaresLandeira_TESE.pdf: 8601965 bytes, checksum: a68be4513e6834f5aaf48800f8ea90d7 (MD5) Previous issue date: 2017-04-11 / O c?rtex cerebral de mam?feros ? histologicamente organizado em diferentes camadas de neur?nios excitat?rios que possuem diversos padr?es de conex?o com alvos corticais e subcorticais. Durante o desenvolvimento, essas camadas corticais se estabelecem sequencialmente atrav?s de uma intrincada combina??o de especifica??o neuronal e migra??o em um padr?o radial conhecida como ?de dentro para fora?: neur?nios infragranulares s?o gerados primeiro do que os neur?nios granulares e supragranulares. Nas ?ltimas d?cadas, diversos genes codificando fatores de transcri??o envolvidos na especifica??o de neur?nios destinados a diferentes camadas corticais foram identificados. Todavia, a influ?ncia dos neur?nios infragranulares sobre a especifica??o das coortes neuronais subsequentes permanece pouco entendida. Para investigar os poss?veis efeitos da abla??o de neur?nios infragranulares sobre a especifica??o de neur?nios supragranulares, n?s induzimos a morte seletiva de neur?nios corticais das camadas V e VI antes da gera??o dos neur?nios destinados ?s camadas II-IV. Nossos dados revelam que um dia ap?s a abla??o, progenitores continuaram a gerar neur?nios destinados a camada VI que expressam o fator de transcri??o TBR1, enquanto praticamente nenhum neur?nio expressando TBR1 foi gerado na mesma etapa do desenvolvimento em controles com a mesma idade. Curiosamente, alguns neur?nios TBR1-positivos gerados ap?s a abla??o de neur?nios infragranulares se estabeleceram em camadas corticais superficiais, como esperado para neur?nios supragranulares gerados neste est?gio, sugerindo que a migra??o de neur?nios corticais pode ser controlada independentemente da sua especifica??o molecular. Al?m disso, n?s observamos um aumento em neur?nios de camada V que expressam CTIP2 e neur?nios calosos que expressam SATB2 ? custa da diminui??o neur?nios de camada IV em animais P0. Quando estes animais se tornam adultos jovens (P30) o aumento de neur?nios SATB2 e CTIP2 n?o existe mais, todavia encontramos esses neur?nios distribu?dos de forma diferente na ?rea somatossensorial dos animais que sofreram abla??o. Experimentos in vitro revelaram que a organiza??o citoarquitet?nica laminar do c?rtex ? necess?ria para gerar novamente os neur?nios TBR1+ que foram eliminados anteriormente. Al?m disso, experimentos in vitro indicam que em condi??o de baixa densidade celular os neur?nios tem seu fen?tipo alterado, expressando v?rios fatores de transcri??o ao mesmo tempo. Em conjunto, nossos dados indicam a exist?ncia de um mecanismo regulat?rio entre neur?nios infragranulares e progenitores envolvidos na gera??o de neur?nios supragranulares e/ou entre neur?nios infragranulares e neur?nios p?s-mit?ticos gerados em seguida. Este mecanismo poderia ajudar a controlar o n?mero de neur?nios em diferentes camadas e contribuir para o estabelecimento de diferentes ?reas corticais. / The cerebral cortex of mammals is histologically organized into in different layers of excitatory neurons that have distinct patterns of connections with cortical or subcortical targets. During development, these cortical layers are sequentially established through an intricate combination of neuronal specification and migration in a radial pattern known as "inside-out": deep-layer neurons are generated prior to upper-layer neurons. In the last few decades, several genes encoding transcription factors involved in the specification of neurons destined to different cortical layers have been identified. However, the influence of early-generated neurons in to the specification of subsequent neuronal cohorts remains unclear. To investigate the possible effects early born neurons ablation on the specification of late born neurons, we induced the selective death of cortical neurons from layers V and VI neurons before the generation of neurons destined to layers II, III and IV. Our data shows that oneday after ablation, progenitors resumed generation of layer VI neurons expressing the transcription factor TBR1, whereas virtually no TBR1-expressing neuron was generated at the same developmental stage in age-matched controls. Interestingly, many TBR1-positive neurons generated after deep-layer ablation settled within superficial cortical layers, as expected for upper-layer neurons generated at that stage, suggesting that migration post-mitotic neurons is independent of fate-specification. Furthermore, we observed an increase in layer V neurons expressing CTIP2 and cortico-cortical neurons expressing SATB2 at the expense of layer IV neurons in P0 animals. When these animals became young adults (P30) the increase os SATB2 and CTIP2 neurons is no longer observed, however these neurons are distributed in a different way in somatosensory areas from ablated animals. In vitro experiments show that the laminar cytoarchitectural organization of the cortex is necessary to regenerate the previously deleted TBR1 + neurons. In addition, in vitro experiments indicate that in a condition of low cell density the neurons phnotype is altered, they express several transcription factors at the same time. Together, our data indicate the existence of feedback mechanism either from early-generated neurons to progenitors involved in the generation of upper-layer neurons or from deep-layer neurons to postmitotic neurons generated subsequently. This mechanism could help to control the number of neurons in different layers and contribute to the establishment of different cortical areas.

Made available in DSpace on 2014-12-17T15:48:00Z (GMT). No. of bitstreams: 1 SimoneOS_DISSERT_capa_ate_pag44.pdf: 4276014 bytes, checksum: c178262769ab9981c0bbfc10faf1c633 (MD5) Previous issue date: 2012-02-10 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers / O desenvolvimento de aplica??es para smart cards requer um alto grau de confiabilidade. M?todos formais fornecem meios para que esta confiabilidade seja alcan?ada. O m?todo e a ferramenta BSmart fornecem uma contribui??o para que o desenvolvimento para smart cards seja feito com o aux?lio do m?todo formal B, gerando c?digo Java Card a partir de especifica??es B. Para que o desenvolvimento com o BSmart seja efetivamente rigoroso sem sobrecarregar o usu?rio do m?todo ? importante que haja uma biblioteca de componentes reutiliz?veis feitos em B. O KitSmart tem como objetivo prover esse aux?lio. Um primeiro estudo sobre a composi??o dessa biblioteca foi tema de uma monografia de gradua??o do curso de Bacharelado em Ci?ncia da Computa??o da Universidade Federal do Rio Grande do Norte, feita por Thiago Dutra em 2006. Esta primeira vers?o do kit resultou na especifica??o dos tipos primitivos permitidos em Java Card (byte, short e boolean) em B e a cria??o de componentes reutiliz?veis para o desenvolvimento de aplica??es. Esta disserta??o prov? o aperfei?oamento do KitSmart com o acr?scimo da especifica??o da API Java Card em B, e um guia para o desenvolvimento de novos componentes. A API Java Card especificada em B, al?m de estar dispon?vel para ser usada no desenvolvimento de projetos, serve como documenta??o ao especificar restri??es de uso para cada classe da API. Os componentes reutiliz?veis correspondem a m?dulos para manipula??o de estruturas espec?ficas, como data e hora, por exemplo. Estes tipos de estruturas n?o est?o dispon?veis em B ou Java Card. Os componentes reutiliz?veis para Java Card s?o gerados a partir das especifica??es verificadas formalmente em B. O guia cont?m informa??es de consulta r?pida para especifica??o de diversas estruturas e como algumas situa??es foram contornadas para adaptar a orienta??o a objetos ao M?todo B. Este trabalho foi avaliado atrav?s de um estudo de caso feito com a ferramenta BSmart que faz uso da biblioteca KitSmart. Neste estudo de caso, ? poss?vel ver a contribui??o dos componentes em uma especifica??o B. Este kit dever? ser ?til tanto para usu?rios do m?todo B como para desenvolvedores de aplica??es Java Card em geral

Made available in DSpace on 2014-12-17T15:28:51Z (GMT). No. of bitstreams: 1 BrunaSL_DISSERT.pdf: 1891001 bytes, checksum: 1d482b920c53ec1f846060dbc2158ebb (MD5) Previous issue date: 2012-08-10 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / The cerebral cortex of mammals is histologically organized into different layers of excitatory neurons that have distinct patterns of connections with cortical or subcortical targets. During development, these cortical layers are established through an intricate combination of neuronal specification and migration in a radial pattern known as "insideout": deep-layer neurons are generated prior to upper-layer neurons. In the last few decades, several genes encoding transcription factors involved in the sequential specification of neurons destined to different cortical layers have been identified. However, the influence of early-generated neurons in the specification of subsequent neuronal cohorts remains unclear. To investigate this possible influence, we induced the selective death of cortical neurons from layer V and VI before the generation of layer II, III and IV neurons. Thus, we can evaluate the effects of ablation of early born neurons on the phenotype of late born neurons. Our data shows that one-day after ablation, layer VI neurons expressing the transcription factor TBR1 are newly generated while virtually no neuron expressing TBR1 was generated in the same age in control animals. This suggests that progenitors involved in the generation of neurons destined for superficial layers suffer interference from the selective death of neurons in deep layers, changing their specification. We also observed that while TBR1-positive neurons are located exclusively in deep cortical layers of control animals, many TBR1-positive neurons are misplaced in superficial layers of ablated animals, suggesting that the migration of cortical neurons could be controlled independently of neuronal phenotypes. Furthermore, we observed an increase in layer V neurons expressing CTIP2 and neurons expressing SATB2 and that these cells have changed their distributions. As a conclusion, our data indicate the existence of a mechanism of control exercised by the early-generated neurons in the cerebral cortex on the fate of the progenitors involved in the generation of the following cortical neurons. This mechanism could help to control the number of neurons in different layers and contribute to the establishment of different cortical areas / O c?rtex cerebral de mam?feros encontra-se histologicamente organizado em camadas de neur?nios excitat?rios que, por sua vez, apresentam distintos padr?es de conectividade com alvos corticais ou sub-corticais. Durante o desenvolvimento, estas camadas corticais s?o estabelecidas atrav?s de uma intrincada combina??o entre especifica??o neuronal e migra??o radial num padr?o conhecido como "inside-out" (de dentro para fora). Desta forma, por exemplo, neur?nios infragranulares nas camadas V e VI s?o gerados anteriormente aos neur?nios granulares da camada IV, que por sua vez s?o gerados antes dos supra-granulares das camadas II e III. Na ?ltima d?cada, foram identificados diversos genes codificando fatores de transcri??o envolvidos na especifica??o sequencial de neur?nios destinados ?s diferentes camadas corticais. No entanto, ainda pouco ? sabido sobre a influ?ncia dos neur?nios gerados previamente sobre a especifica??o das coortes neuronais subsequentes. Para investigar esta poss?vel influ?ncia, n?s utilizamos um m?todo de recombina??o g?nica (sistema Cre- Lox) para induzir a morte seletiva de neur?nios das camadas corticais V e VI antes da gera??o dos neur?nios das camadas II, III e IV. Dessa forma, pudemos avaliar os efeitos da abla??o de neur?nios infragranulares sobre o fen?tipo dos neur?nios gerados em seguida. Nossos dados mostraram que, um dia ap?s a abla??o, neur?nios da camada VI expressando o fator de transcri??o TBR1 voltaram a ser gerados enquanto praticamente nenhum neur?nio expressando TBR1 foi gerado na mesma idade em animais controle. Esse dado sugere que os progenitores envolvidos na gera??o de neur?nios destinados ?s camadas superficiais sofrem interfer?ncia da morte seletiva de neur?nios de camadas profundas, mudando sua especifica??o. Uma parte dos neur?nios TBR1 se estabeleceu na camada VI e outra migrou at? as camadas II e III, indicando que o controle dos padr?es migrat?rios pode ser independente dos fen?tipos neuronais. Al?m disso, observamos que na popula??o neuronal total tamb?m ocorreu um aumento na quantidade de neur?nios de camada V expressando CTIP2 e uma altera??o na distribui??o dessas c?lulas. O mesmo foi observado para neur?nios supragranulares expressando SATB2. Em conjunto, nossos dados indicam a exist?ncia de um mecanismo de controle exercido pelos neur?nios gerados inicialmente no c?rtex cerebral sobre o destino dos progenitores envolvidos na gera??o dos demais neur?nios corticais. Tal mecanismo poderia contribuir para o controle do n?mero de neur?nios em diferentes camadas e contribuir para o estabelecimento de diferentes ?reas corticais

Made available in DSpace on 2014-12-17T15:47:56Z (GMT). No. of bitstreams: 1 DiegoHOS_DISSERT.pdf: 2899752 bytes, checksum: d3160b774efd6749eced9bb34d4a74cf (MD5) Previous issue date: 2011-08-31 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the system s properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++. / Usando m?todos formais, o desenvolvedor pode aumentar a confiabilidade e corretude do software. Al?m disso, o desenvolvedor pode concentrar-se mais nos requisitos funcionais. Por?m h? muita resist?ncia em se adotar essa abordagem de desenvolvimento de software. A raz?o principal e a escassez de suporte ferramental adequado, ?til e de f?cil utiliza??o. Os desenvolvedores normalmente escrevem o c?digo e o testam. Estes testes geralmente consistem em checar se as sa?das est?o de acordo com os requisitos. Isto, contudo, nem sempre e poss?vel de maneira exaustiva. Por outro lado, usando M?todos Formais um desenvolvedor e capaz de investigar profundamente as propriedades do sistema. Infelizmente, linguagens de especifica??o formal nem sempre possuem ferramentas como animador ou simulador e ?s vezes n?o h? interfaces gr?ficas amig?veis. Por?m, algumas dessas ferramentas possuem um compilador, que gera um Sistema de Transi??es Rotuladas (LTS). A proposta deste trabalho ? desenvolver um aplicativo que fornece anima??o gr?fica para especifica??es formais usando o LTS como entrada. O aplicativo inicialmente suporta as as linguagens B, CSP e Z. Usando o LTS em um formato XML especificado ? poss?vel animar outras linguagens formais. Adicionalmente a ferramenta disponibiliza visualiza??o de traces, escolhas feitas pelo usu?rio, em um formato de ?rvore gr?fica. A inten??o ? melhorar a compreens?o de uma especifica??o, fornecendo informa??es sobre erros e animando-a, como os desenvolvedores fazem com linguagens de programa??o como Java e C++.