Made available in DSpace on 2014-06-12T17:16:32Z (GMT). No. of bitstreams: 2 arquivo558_1.pdf: 1430817 bytes, checksum: a4b16d2e9a8f62f0f5c40945bbb618fb (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2008 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / Pode-se definir Capital Humano como os atributos que as pessoas têm ou adquirem que as tornam mais produtivas no contexto econômico. A despeito da dimensão do conceito, a literatura do crescimento econômico tem como praxe utilizar as variáveis de escolaridade para representar tal forma de capital. Utilizando um conceito de Capital Humano mais abrangente, que incorpora tanto aspectos qualitativos, quanto aspectos quantitativos da escolaridade, esse trabalho busca construir indicadores de pobreza educacional para as Unidades Federativas do Brasil. Pode-se dizer que existe pobreza educacional quando uma ou mais pessoas não atingem um nível mínimo necessário de escolaridade para os padrões da sociedade em questão, em outras palavras, esse conceito é análogo ao conceito de pobreza. Partindo da idéia que o estoque de Capital Humano é um dos componentes do bem-estar, combater a pobreza educacional é uma forma de aumentar o bem-estar de uma sociedade. Assim, os objetivos da tese são: construir um indicador de capital humano incorporando aspectos quantitativos e qualitativos da escolaridade, que segundo Schultz (1964) é o maior componente do investimento em capital humano; construir indicadores de pobreza educacional, buscando estudar as camadas inferiores da distribuição da educação; e por fim utilizar a abordagem do valor de Shapley para decompor a Pobreza Educacional por subgrupos (idade, sexo, raça), a fim de investigar quais os mais afetados em cada Unidade Federativa do Brasil. É importante ressaltar que o método de decomposição de Shapley generalizado por Shorrocks (1999) permite identificar a participação de cada subgrupo separadamente num procedimento de decomposição simultâneo, e que até a generalização proposta por Shorrocks (1999) não era possível separar a contribuição de cada subgrupo num procedimento desse tipo. De forma geral, os resultados encontrados apontam para o sucesso das políticas educacionais dos últimos anos que visavam aumentar o acesso à escolaridade, no entanto, percebe-se que as disparidades regionais relacionadas à escolaridade se mantiveram nos anos analisados (1996 e 2006)

O constante aumento da velocidade de processamento, devido principalmente à utilização de um número cada vez maior de processadores, tem propiciado grandes avanços no projeto e na construção de sistemas computacionais paralelos. Entretanto o desempenho de muitas aplicações é afetado pela latência das operações de Entrada e Saída de dados. Para solucionar esse problema, sistemas de arquivos paralelos, que oferecem acesso paralelo aos dados armazenados em diversos discos, vêm sendo desenvolvidos. O desenvolvimento desses sistemas complexos pode ser beneficiado pela adoção de Técnicas de Descrição Formal (TDFs), durante as fases de projeto e especificação dos mesmos, as quais podem ser aliadas a técnicas de implementação durante as demais fases. Neste sentido, este projeto propõe uma abordagem baseada em frameworks e na TDF Extended State Transition Language (Estelle), para a especificação formal, validação, implementação e teste de sistemas dessa categoria. Um framework conceitual que descreve um sistema funcional é apresentado, e dois estudos de caso são desenvolvidos dando origem a dois sistemas de arquivos derivados do framework. Uma metodologia para a validação, que usa ferramentas de simulação, é apresentada. Um dos estudos de caso é implementado semi-automaticamente, a partir de sua especificação formal Estelle, e comparações de desempenho com o mesmo sistema implementado manualmente são realizadas. / The constant increase of processing speed, mainly due to the use of a large number of processors, has allowed an improvement in the design and building of parallel computation systems. However, the performance of several types of applications is affected by the latency originated from Input/Output operations on data. In order to solve this problem parallel file systems, which allow parallel access to the data stored on a set of discs, have been developed. The design of such complex systems can benefit from the adoption of implementation techniques allied with Formal Description Techniques (FDTs). Aimed to introduce the use of FDTs in the development cycle of distributed parallel file systems, this work proposes an approach, based on framework and the FDT Extended State Transition Language (Estelle), for the formal specification, validation, implementation and testing of systems belonging to this domain. A conceptual framework that describes a basic functional system is presented, and two case studies are developed from it. A methodology for Estelle specification validation that makes use of simulation tools is also proposed in this work. One of the systems, developed as a case study, is semi-automatically implemented from its Estelle formal specification, and performance comparisons with a hand-coded implementation of the same system are done.

Este trabalho de pesquisa propõe um método orientado a processo para elicitação de requisitos, visando melhorar a compreensão de negócios e reduzir informações erradas ou omitidas, bem como os conflitos de visões e propagações de erros no desenvolvimento de Sistemas Computadorizados (SCs). O método proposto encontra-se estruturado em duas fases: Preparação dos Modelos de Negócio e Elicitação de Requisitos. Na fase de Preparação dos Modelos de Negócio, foram customizados, tanto os critérios para validação do Diagrama de Processo de Negócio (Business Process Diagram - BPD), quanto o modelo executável da especificação da Notação da Modelagem de Processos de Negócio (Business Process Modeling Notation - BPMN). O método proposto foi validado em um estudo de caso, envolvendo um processo de negócio real no Centro de Serviços Compartilhados (CSC) da Fundação São Francisco Xavier (FSFX), em Ipatinga, Minas Gerais, Brasil. Ele representa a principal contribuição desta pesquisa. Além disso, algumas contribuições complementares da fase de Elicitação de Requisitos são: a elicitação de requisitos padronizados, não ambíguos e alinhados às necessidades dos stakeholders; a extração e mapeamento de regras de negócio; a priorização e rastreabilidade de requisitos; a customização dos critérios de validação de BPD; a customização do modelo executável da BPMN; e a aplicação do método proposto no estudo de caso.

O constante aumento da velocidade de processamento, devido principalmente à utilização de um número cada vez maior de processadores, tem propiciado grandes avanços no projeto e na construção de sistemas computacionais paralelos. Entretanto o desempenho de muitas aplicações é afetado pela latência das operações de Entrada e Saída de dados. Para solucionar esse problema, sistemas de arquivos paralelos, que oferecem acesso paralelo aos dados armazenados em diversos discos, vêm sendo desenvolvidos. O desenvolvimento desses sistemas complexos pode ser beneficiado pela adoção de Técnicas de Descrição Formal (TDFs), durante as fases de projeto e especificação dos mesmos, as quais podem ser aliadas a técnicas de implementação durante as demais fases. Neste sentido, este projeto propõe uma abordagem baseada em frameworks e na TDF Extended State Transition Language (Estelle), para a especificação formal, validação, implementação e teste de sistemas dessa categoria. Um framework conceitual que descreve um sistema funcional é apresentado, e dois estudos de caso são desenvolvidos dando origem a dois sistemas de arquivos derivados do framework. Uma metodologia para a validação, que usa ferramentas de simulação, é apresentada. Um dos estudos de caso é implementado semi-automaticamente, a partir de sua especificação formal Estelle, e comparações de desempenho com o mesmo sistema implementado manualmente são realizadas. / The constant increase of processing speed, mainly due to the use of a large number of processors, has allowed an improvement in the design and building of parallel computation systems. However, the performance of several types of applications is affected by the latency originated from Input/Output operations on data. In order to solve this problem parallel file systems, which allow parallel access to the data stored on a set of discs, have been developed. The design of such complex systems can benefit from the adoption of implementation techniques allied with Formal Description Techniques (FDTs). Aimed to introduce the use of FDTs in the development cycle of distributed parallel file systems, this work proposes an approach, based on framework and the FDT Extended State Transition Language (Estelle), for the formal specification, validation, implementation and testing of systems belonging to this domain. A conceptual framework that describes a basic functional system is presented, and two case studies are developed from it. A methodology for Estelle specification validation that makes use of simulation tools is also proposed in this work. One of the systems, developed as a case study, is semi-automatically implemented from its Estelle formal specification, and performance comparisons with a hand-coded implementation of the same system are done.

Submitted by Marcio Filho (marcio.kleber@ufba.br) on 2016-06-07T13:18:22Z No. of bitstreams: 1 dissertacao_anderson.pdf: 550160 bytes, checksum: 330886b135074855963d7424f479f579 (MD5) / Approved for entry into archive by Uillis de Assis Santos (uillis.assis@ufba.br) on 2016-06-07T18:56:58Z (GMT) No. of bitstreams: 1 dissertacao_anderson.pdf: 550160 bytes, checksum: 330886b135074855963d7424f479f579 (MD5) / Made available in DSpace on 2016-06-07T18:56:58Z (GMT). No. of bitstreams: 1 dissertacao_anderson.pdf: 550160 bytes, checksum: 330886b135074855963d7424f479f579 (MD5) / Rufus Bowen, em seu artigo publicado em 1971, mostrou que, dado f um difeomorfismo Axioma A, seu conjunto não errante pode ser decomposto em uma quantidade finita de subconjuntos distintos. Analisando f restrita a cada um desses subconjuntos ele notou uma propriedade muito interessante: dada uma quantidade finita de trechos finitos de órbitas dessa restrição de f, sempre existia um ponto periódico cuja órbita aproximava esses dados trechos. A essa propriedade denotamos por especificação. Notou-se entretanto que este tipo de fenômeno não se restringia a classe de difeomorfismos Axioma A. Temos, por exemplo, que toda aplicação topologicamente mixing no intervalo e toda aplicação conjugada a um shift completo satisfaz a propriedade de especificação. A partir de então, a noção de especificação tornou-se uma ferramenta muito útil na teoria ergódica. No presente trabalho, apresentamos duas consequências da propriedade de especificação. A primeira é uma caracterização topológica do espaço de medidas invariantes mostrada por Karl Sigmund em 1974. Com esta caracterização destacam-se alguns subconjuntos interessantes, como o de medidas com suporte em uma órbita periódica, o de medidas ergódicas, não atômicas e abertas. A segunda consequência é que se f satisfaz a pro- priedade de especificação, então o conjunto dos pontos cujas médias de Birkhoff para um dado potencial contínuo ϕ não convergem ou é vazio ou tem pressão topológica total, resultado devido a Daniel Thompson em 2010.

Dissertação (mestrado)—Universidade de Brasília, Institudo de Ciências Exatas, Departamento de Ciência da Computação, 2014. / Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2014-10-21T13:01:44Z No. of bitstreams: 1 2014_ArianeAlvesAlmeida.pdf: 1238432 bytes, checksum: 443ba143f22122e23f5542311f804fe9 (MD5) / Approved for entry into archive by Tania Milca Carvalho Malheiros(tania@bce.unb.br) on 2014-10-22T15:32:03Z (GMT) No. of bitstreams: 1 2014_ArianeAlvesAlmeida.pdf: 1238432 bytes, checksum: 443ba143f22122e23f5542311f804fe9 (MD5) / Made available in DSpace on 2014-10-22T15:32:03Z (GMT). No. of bitstreams: 1 2014_ArianeAlvesAlmeida.pdf: 1238432 bytes, checksum: 443ba143f22122e23f5542311f804fe9 (MD5) / Uma abordagem é apresentada para verificar formalmente a corretude lógica de operadores algébricos implementados em hardware. O processo de verificação é colocado em paralelo ao fluxo convencional de projeto de hardware, permitindo a verificação de fragmentos da implementação do hardware tanto simultaneamente quanto após todo o processo de implementação ser concluído, evitando assim atrasos no projeto do circuito. A ideia principal para atestar a corretude de uma implementação em hardware é comparar seu comportamento operacional com uma definição formal de seu operador, analisando assim sua equivalência funcional; isto é, se ambas definições, de hardware e matemática, produzem os mesmos resultados quando fornecidas as mesmas entradas. A formalização dessa comparação é um desafio desta abordagem, já que as provas utilizadas para verificar a corretude e outras propriedades desses sistemas pode seguir esquemas indutivos, que proveem de maneira natural quando se trata com definições recursivas, usadas em linguagens de especificação e ferramentas de formalização. Já que Linguagens de Descrição de Hardware descrevem circuitos/sistemas de maneira imperativa, a abordagem se baseia na tradução conservativa de comandos iterativos presentes nessas linguagens em suas respectivas especificações recursivas. Esses esquemas de provas indutivas são baseados em garantir pré e pós-condições, bem como a preservação de invariantes durante todos os passos da execução recursiva, de acordo com a abordagem da lógica de Floyd-Hoare para verificação de procedimentos imperativos. A aplicabilidade da metodologia é ilustrada com um caso de estudo utilizando o assistente de prova de ordem superior PVS para fornecer prova de correção lógica de uma implementação em FPGA do algoritmo para inversão de matrizes de Gauss-Jordan (GJ). Essas provas em PVS são dadas em um estilo dedutivo baseado no Cálculo de Gentzen, aproveitando facilidades desse assistente, como tipos dependentes, indução na estrutura de tipos de dados abstratos e, é claro, suas linguagens de especificação e prova em lógica de ordem superior. ________________________________________________________________________________ ABSTRACT / An approach is introduced to formally verify the logical correctness of hardware implementations of algebraic operators. The formal verification process is placed sidelong the usual hardware design flow, allowing verification on fragments of the hardware implementation either simultaneously or after the whole implementation process finished, avoiding in this way hardware development delays. The main idea to state the correctness of a hardware implementation, is to compare its operational behavior with a formal definition of the operator, analysing their functional equivalence; that is, if both the hardware and the mathematical definition produce the same results when provided with the same entries. The formalization of this comparison is a challenge for this approach, since the proofs used to verify soundness and other properties of these systems might follow inductive schemata, that arise in a natural manner when dealing with recursive definitions, used in specifications languages of formalization tools. Since Hardware Description Languages describe circuits/systems in an imperative style, the approach is based on a conservative translation of iterative commands into their corresponding recursive specifications. The inductive proof schemata are then based on guaranteeing pre and post-conditions as well as the preservation of invariants during all steps of the recursive execution according to the Floyd-Hoare’s logical approach for verification of imperative procedures. The applicability of the methodology is illustrated with a case study using the higher-order proof assistant PVS by proving the logical correction of an FPGA implementation of the Gauss-Jordan matrix inversion algorithm (GJ). These PVS proofs are given in a Gentzen based deductive style taking advantage of nice features of this proof assistant such as dependent types and induction in the structure of abstract data types, and, of course, of its higher-order specification and proof languages.

Made available in DSpace on 2014-06-12T16:01:30Z (GMT). No. of bitstreams: 2 arquivo9418_1.pdf: 2222541 bytes, checksum: b014d66f1d25c6852ecac19fa19003b7 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Muitos dos problemas encontrados no uso do mecanismo de tratamento de exceções são causados pela falta de projeto e teste do comportamento excepcional de um sistema em fases iniciais do desenvolvimento de software. Como consequência, exceções são propagadas de forma inesperada durante causando impacto negativo na confiabilidade de um software. Neste trabalho apresentamos uma abordagem que possibilita projetar testes desde as atividades iniciais do desenvolvimento e verificar, em tempo de execução, como as exceções trafegam ao longo de um sistema. Através da especificação do fluxo excepcional esperado é possível determinar se uma exceção foi propagada corretamente. Um segundo uso desta abordagem destina-se ao auxilio das atividades de manutenção de um sistema. Para isto, uma versão inicial existente é especificada e os testes são executados nas novas versões ao longo da evolução do sistema. Com isso é possível verificar a consistência do comportamento excepcional a cada nova versão. Um benefício da abordagem proposta deve-se ao fato de que os testes escritos servem como a própria documentação viva do sistema mantendo-a sempre atualizada. Para a avaliação desta abordagem foram selecionados três sistemas: aTunes, jEdit e Health Watcher. Através do seu uso foram descobertos dezesseis bugs. Deste total doze foram erros inéditos não reportados na base de bugs destes projetos. Não somente bugs foram descobertos com a utilização desta abordagem. Do ponto de vista de testes automatizados, como artefatos de documentação, foram apontadas diversas diferenças entre as versões dos sistemas com relação aos fluxos excepcionais testados. Para auxiliar a automação dos testes, a abordagem foi implementada como uma extensão do framework JUnit. Os testes especificados nesta extensão contém informações complementares sobre o fluxo excepcional esperado

Um novo modelo para a especificação de hiperdocumentos denominado HMBS - Hyperdocument Model Based on Statecharts - é proposto. O HMBS adota como modelo formal subjacente a técnica Statecharts, cuja estrutura e semântica operacional são utilizadas para especificar a estrutura organizacional e a semântica de navegação de hiperdocumentos grandes e complexos. A definição do HMBS, bem como a semântica de navegação adotada, são apresentadas. Na definição apresenta-se como o modelo permite separar as informações referentes a estrutura organizacional e navegacional das representações físicas do hiperdocumento. Também são discutidas características do modelo que possibilitam ao autor analisar a estrutura do hiperdocumento, encorajando a especificação de hiperdocumentos estruturados. Para provar e validar a viabilidade prática do uso do HMBS num contexto real foi desenvolvido um ambiente de autoria e navegação de hiperdocumentos denominado HySCharts - Hyperdocumenf System based on Statecharts. Esse ambiente fornece facilidades de prototipação rápida e simulação interativa de hiperdocumentos. Para ilustrar como o modelo HMBS e o HySCharts podem ser utilizados no contexto de uma abordagem de projeto sistemática é utilizada como estudo de caso a especificação de um hiperdocumento que apresenta o Parque Ecológico de São Carlos / A new model for hyperdocument specification called HMBS - Hyperdocument Model Based on Statecharts - is proposed. HMBS uses the Statechart formalism as its underlying model. Statecharts structure and operational semantics are used to specify the organizational structure and the browsing semantics of large and complex hyperdocuments. The definition of HMBS is presented and its browsing semantics is described. It is shown how the model allows the separation of information related to the organizational and navigational structure from the hyperdocument\'s physical representation. Model features that allow authors to analyze the hyperdocument structure, encouraging the specification of structured hyperdocuments are also discussed. As a proof of concept and also to evaluate the feasibility of using HMBS in real-life applications a system called HySCharts - Hyperdocument System based on StateCharts - was developed. HySCharts is composed by an authoring and a browsing environments, supporting rapid prototyping and interactive simulation of hyperdocuments. A case study is presented that uses the specification of a hyperdocument introducing the Ecological Park of São Carlos to illustrate the use of HMBS and of the HySCharts environment integrated into a systematic design approach

Foi definido que elementos regulatórios da expressão atrial-específica do promotor da SMyHC3 estão contidos em um elemento complexo de resposta a receptores nucleares (ECRRN). Ensaios de transativação celular indicam que alguns receptores nucleares se ligam nesta região. A partir destes ensaios verificamos a ativação do promotor por um receptor nuclear, o COUP-TFII. Ele regula muitos processos biológicos, como angiogênese e o próprio desenvolvimento atrial. Através da deleção do ECRRN observamos que o promotor não era ativado por COUP-TFII, indicando a sua ligação nessa região. Verificamos ainda que somente o domínio de ligação ao ligante do COUP-TFII é capaz de ativar o promotor, sugerindo a necessidade de uma interação com outros RNs para ativar o promotor. Uma análise proteômica indica que a maioria dos interactores de COUP-TFII está relacionada com complexos reguladores da transcrição e com a via de sinalização do receptor de andrógenos (AR). Ensaios de transativação celular mostram que juntos, COUP-TFII e AR, são capazes de aumentar a ativação do promotor. / It was determined that regulatory elements of the atrial-specific expression of the promoter SMyHC3 are contained in a complex nuclear receptor response element (CNRRE). Cellular transactivation assays indicated certain nuclear receptors (NR) can bind in this region. From these trials, was observed the promoter activation by a nuclear receptor, COUP-TFII. It regulates many biological processes such as angiogenesis and atrial development. Deletion of CNRRE resulted in no activation of the promoter by COUP-TFII, indicating their connection in this region. We also verified that only the ligand binding domain of COUP-TFII is able to activate the promoter, suggesting interaction with other NRs to activate it. A proteomic analysis revealed that most of COUP-TFII partners relates to complexes of transcription regulators and the androgen receptor (AR) signaling pathway. Cell transactivation assays showed that together, COUP - TFII and AR, are able to increase promoter activation.

Com a presença cada vez maior de sistemas computacionais e novas tecnologias no cotidiano das pessoas, garantir que eles não falhem e funcionem corretamente tornou-se algo de extrema importância. Além de indicar a qualidade do sistema, assegurar seu bom funcionamento é essencial para se evitar perdas, desde financeiras até de vidas. Uma das técnicas utilizadas para esta finalidade é a chamada verificação formal de programas. A partir da especificação do sistema, descrita numa linguagem formal, são definidas propriedades a serem satisfeitas e que certificariam a qualidade do software. Estas propriedades devem então ser implementadas para uso num verificador, que é a ferramenta responsável por executar a verificação e informar quais propriedades foram satisfeitas e quais não foram; no caso das propriedades terem sido violadas, o verificador deve indicar aos desenvolvedores os possíveis locais com código incorreto no sistema. A desvantagem do uso da verificação formal é, além do seu alto custo, a necessidade de haver pessoas com experiência em métodos formais para definir propriedades a partir da especificação formal do sistema, e convertê-las numa representação que possa ser entendida pelo verificador. Este processo de definição de propriedades é particularmente complexo, demorado e suscetível a erros, por ser feito em sua maior parte de forma manual. Para auxiliar os desenvolvedores na utilização da verificação formal em programas escritos em Java, propomos neste trabalho a geração de representação de propriedades para uso direto num verificador. As propriedades a serem geradas são objetivos de teste derivados da especificação formal do sistema. Estes objetivos de teste descrevem o comportamento esperado do sistema que deve ser observado durante sua execução. Ao estabelecer que o universo de propriedades corresponde ao universo de objetivos de teste do programa, garantimos que as propriedades geradas em nosso trabalho descrevem o comportamento esperado do programa por meio de caminhos de execução que levam a um estado de aceitação da propriedade, ou a um estado de violação. Assim, quando o verificador checa o objetivo de teste, ele consegue dar como resultado o veredicto de sucesso ou falha para a propriedade verificada, além de dados da cobertura dos caminhos de execução do programa que podem ser usados para análise do comportamento do programa que levou ao sucesso ou falha da propriedade verificada. / The task of guaranteeing that computational systems do not fail and work correctly has become extremely important with the growing presence of new technologies in people\'s lives. Therefore, it is essential to ensure that such systems work properly to confirm their high-quality and to avoid financial and even life losses. One of the techniques used to this purpose is called formal verification of programs. From the system specification, which should be described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties are checked using a verifier, which is the tool responsible for running the verification and for notifying whether the property was satisfied by the program; if the property was violated, it indicates to software developers the possible location of faults in the system. The disadvantages of using formal verification are the high cost to apply this technique in practice, and the necessity of having people with experience in formal methods to derive the properties from system specification and define them in a formal representation that can be read by a program verifier. This particular task of deriving a property from system specification and defining it to be checked by a verifier is complex, time-consuming and error-prone, since it is usually done by hand. To help software developers in the application of formal verification in Java programs, we propose in this work the generation of properties formal representation for direct use in a verifier. The generated properties are test purposes, which are derived from system formal specification and present the desirable system behavior that must be observed during the system execution. Establishing that the universe of properties correspond to the universe of test purposes of a program, we guarantee that the generated properties describe the expected program behavior through execution traces that lead to either an accept state or a refuse state. Thus, when the verifier checks the test purpose, it can give a success/fail verdict for the property, and provide traces coverage data that can be used to analyze the program behavior that led to that verdict.