Tese de Mestrado Integrado. Engenharia Civil. Faculdade de Engenharia. Universidade do Porto. 2011

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.

Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2017. / Submitted by Raquel Almeida (raquel.df13@gmail.com) on 2017-12-22T10:53:47Z No. of bitstreams: 1 2017_AndréLuizPeronMartinsLanna.pdf: 4218714 bytes, checksum: a2374ea747f76f8e47ee2377c3a3a989 (MD5) / Approved for entry into archive by Raquel Viana (raquelviana@bce.unb.br) on 2018-02-15T20:00:30Z (GMT) No. of bitstreams: 1 2017_AndréLuizPeronMartinsLanna.pdf: 4218714 bytes, checksum: a2374ea747f76f8e47ee2377c3a3a989 (MD5) / Made available in DSpace on 2018-02-15T20:00:30Z (GMT). No. of bitstreams: 1 2017_AndréLuizPeronMartinsLanna.pdf: 4218714 bytes, checksum: a2374ea747f76f8e47ee2377c3a3a989 (MD5) Previous issue date: 2018-02-15 / Contexto: Técnicas de verificação têm sido aplicadas para garantir que sistemas de software atinjam níveis de qualidade desejados e atenda a requisitos funcionais e nãofuncionais. Entretanto a aplicação dessas técnicas de verificação em linhas de produto de software é desafiador devido à explosão combinatorial do número de produtos que uma linha de produtos pode instanciar. As técnicas atuais de verificação de linhas de produtos utilizam model checking simbólico e informações sobre variabilidade para otimizar a análise, mas ainda apresentam limitações que as tornam onerosas ou inviáveis. Em particular, as técnicas de verificação do estado da arte para análise de confiabilidade em linhas de produto são enumerativas o que dificulta a aplicabilidade das mesmas devido à explosão combinatorial do espaço de configurações. Objetivo: Os objetivos dessa tese são os seguintes: (a) apresentar um método eficiente para calcular a confiabilidade de todas as configurações de uma linha de produtos de sotware composicional ou anotacional à partir de seus modelos comportamentais UML, (b) fornecer uma ferramenta que implemente o método proposto e, (c) relatar um estudo empírico comparando o desempenho de diferentes estratégias de análises de confiabilidade para linhas de produto de software. Método: Esse trabalho apresenta uma nova estratégia de análise feature-family-based para calcular a confiabilidade de todos os produtos de uma linha de produtos de software (composicional ou anotacional). O passo feature-based da estratégia divide os modelos comportamentais em unidades menores para que essas possam ser analisadas mais eficientemente. O passo family-based realiza o cálculo de confiabilidade para todas as configurações de uma só vez ao avaliar as expressões de confiabilidade em termos de uma estrutura de dados variacional adequada. Resultados: Os resulstados empíricos mostram que a estratégia feature-family-based para análise de confiabilidade supera, em termos de tempo e espaço, quatro outras estratéfias de análise do estado da arte (product-based, family-based, feature-product-based e family-product-based) para a mesma propriedade. No contexto da avaliação e em comparação com as outras estratégias, a estratégia feature-family-based foi a única capaz de escalar a um crescimento do espaço de configuração da ordem de 220. Conclusões: A estratégia feature-family-based utiliza e se beneficia das estratégias feature- e family- ao domar o crescimento dos tamanhos dos modelos a serem analizados e por evitar a enumeração de produtos inerentes a alguns métodos de análise do estado da arte. / Context: Verification techniques are being applied to ensure that software systems achieve desired quality levels and fulfill functional and non-functional requirements. However, applying these techniques to software product lines is challenging, given the exponential blowup of the number of products. Current product-line verification techniques leverage symbolic model checking and variability information to optimize the analysis, but still face limitations that make them costly or infeasible. In particular, state-of-the-art verification techniques for product-line reliability analysis are enumerative which hinders their applicability, given the latent exponential blowup of the configuration space. Objective: The objectives of this thesis are the following: (a) we present a method to eciently compute the reliability of all configurations of a compositional or annotationbased software product line from its UML behavioral models, (b) we provide a tool that implements the proposed method, and (c) we report on an empirical study comparing the performance of dierent reliability analysis strategies for software product lines. Method: We present a novel feature-family-based analysis strategy to compute the reliability of all products of a (compositional or annotation-based) software product line. The feature-based step of our strategy divides the behavioral models into smaller units that can be analyzed more eciently. The family-based step performs the reliability computation for all configurations at once by evaluating reliability expressions in terms of a suitable variational data structure. Results: Our empirical results show that our feature-family-based strategy for reliability analysis outperforms, in terms of time and space, four state-of-the-art strategies (product-based, family-based, feature-product-based, and family-product-based) for the same property. In the evaluation’s context and in comparison with the other evaluation strategies, it is the only one that could be scaled to a 220-fold increase in the size of the configuration space. Conclusion: Our feature-family-based strategy leverages both feature- and familybased strategies by taming the size of the models to be analyzed and by avoiding the products enumeration inherent to some state-of-the-art analysis methods.

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciências da Computação, 2015. / Submitted by Ana Cristina Barbosa da Silva (annabds@hotmail.com) on 2015-07-01T17:56:17Z No. of bitstreams: 1 2015_NilsonDonizeteGuerinJunior.pdf: 6113923 bytes, checksum: 78389d648276fe440825b587503b2213 (MD5) / Approved for entry into archive by Raquel Viana(raquelviana@bce.unb.br) on 2015-07-17T11:47:21Z (GMT) No. of bitstreams: 1 2015_NilsonDonizeteGuerinJunior.pdf: 6113923 bytes, checksum: 78389d648276fe440825b587503b2213 (MD5) / Made available in DSpace on 2015-07-17T11:47:21Z (GMT). No. of bitstreams: 1 2015_NilsonDonizeteGuerinJunior.pdf: 6113923 bytes, checksum: 78389d648276fe440825b587503b2213 (MD5) / O reconhecimento biométrico pode ser definido como a ciência de estabelecer a identidade de um indivíduo baseado nas características físicas e/ou comportamentais da pessoa seja de maneira totalmente automática seja de forma semiautomática. Um sistema biométrico tem dois tipos de funcionalidades: a verificação e a identificação. Na verificação, o usuário afirma sua identidade e o sistema verifica se a afirmação é genuína. A identificação diz respeito a apontar uma identidade, dentre todas as cadastradas no sistema, para uma amostra de entrada. A biometria tem vantagens sobre abordagens baseadas em tokens ou conhecimento de informações (por exemplo, uma senha). Isto porque tokens podem ser perdidos e o conhecimento pode ser esquecido. O reconhecimento de escritor baseado em texto é uma das áreas mais ativas na biometria, dentre as biometrias comportamentais. Tanto as abordagens online quanto offline tem sido estudadas em trabalhos anteriores. Mas quando se refere ao tipo de texto usado, o reconhecimento de assinatura tem atraído muito mais atenção do que abordagens baseadas em outros tipos de escrita, especialmente no caso online. Além disso, o cenário com dispositivos móveis foi pouco abordado nesse contexto. O objetivo deste trabalho é o desenvolvimento de um sistema de verificação multibiométrica aplicável a palavras cursivas isoladas e assinaturas, em um cenário com dispositivos móveis. Uma base de dados, denominada LISA-01, foi especialmente desenvolvida para avaliar o cenário desejado. O sistema considera descritores de Fourier, histogramas e velocidade para classificação, tendo em vista baixa complexidade computacional. Foram desenvolvidas e avaliadas duas propostas para otimização no uso de histogramas. Taxas de erro de 6,47% e 4,39% são obtidas nas bases de dados LISA-01 e MCYT-100, respectivamente. Os resultados sugerem que a combinação das características utilizadas é complementar e que o uso de palavras cursivas isoladas pode ser adequado em sistemas biométricos. Além disso, evidenciam que há relevância entre comprimento da palavra e a performance de verificação. / The biometric recognition can be defined as the science of establishing the identity of an individual based on physical and / or behavioral characteristics of the person in a fully or semiautomatic way. A biometric system has two types of taks: verification and identification. In verification, the user claim his/her identity and the system checks whether the claim is genuine. Identification concerns about relating a sample to an identity among all registered in the system. Biometrics has advantages over approaches based on tokens or knowledge (e.g. passwords) as tokens can be lost and knowledge can be forgotten. The recognition of writer based on text is one of the most active areas in biometrics, specifically in the behavioral biometrics. Both online and offline approaches have been studied in previous work. But when it comes to the type of text used, the signature recognition has attracted much more attention than approaches based on other types of writing, especially in the case online. In addition, the scenario with mobile devices was not much discussed in this context. The objective of this work is the development of a multi-biometric verification system applicable to isolated cursive words and signatures, in a scenario with mobile devices. A database, called LISA-01, was specially developed to evaluate the desired scenario. The system considers Fourier descriptors, velocity and histograms for classification, obtaining low computational complexity. Proposals for optimizing the use of histograms is also developed and evaluated. Error rates of 6.47% and 4.39% are obtained in the database LISA-01 and MCYT- 100, respectively. The results suggest that the combination of the used characteristics is complementary and the introduction of isolated cursive words can be appropriate to biometric systems. Furthermore, the relevance of word length on verification performance is also identified.

Made available in DSpace on 2016-08-29T15:33:14Z (GMT). No. of bitstreams: 1 tese_4141_.pdf: 1818467 bytes, checksum: c5ab298abcaaed9ba910c91cbc9e8982 (MD5) Previous issue date: 2010-08-31 / A tarefa de reconhecimento facial é uma das tarefas mais corriqueiras e naturais executadas pelos seres humanos. Apesar de simples para nós, esta tarefa tem se mostrado um grande desafio para pesquisadores nas áreas de inteligência artificial e visão computacional. As pesquisas na área de detecção e reconhecimento de objetos, e mais especificamente aquelas voltadas à face humana, têm aumentado muito nos últimos anos principalmente devido à sua aplicabilidade em áreas tais como: segurança pública, controle de acesso, autenticação continua em redes de computadores, entre outras. Nesta dissertação, investigamos a viabilidade de um sistema para controle de acesso que usa unicamente a biometria da face como chave de acesso. Neste caso, o controle de acesso deixa de ser baseado em algo que o individuo tem ou algo que o individuo sabe e passa a ser baseado no próprio indivíduo.

Dissertação (mestrado)—Universidade de Brasília, Instituto de Geociências, 2015. / Submitted by Fernanda Percia França (fernandafranca@bce.unb.br) on 2016-03-03T15:22:46Z No. of bitstreams: 1 2015_BrunaCardosoMendes.pdf: 3701029 bytes, checksum: cefe79e25582b635c5321cf2c091404f (MD5) / Approved for entry into archive by Guimaraes Jacqueline(jacqueline.guimaraes@bce.unb.br) on 2016-04-07T11:22:06Z (GMT) No. of bitstreams: 1 2015_BrunaCardosoMendes.pdf: 3701029 bytes, checksum: cefe79e25582b635c5321cf2c091404f (MD5) / Made available in DSpace on 2016-04-07T11:22:06Z (GMT). No. of bitstreams: 1 2015_BrunaCardosoMendes.pdf: 3701029 bytes, checksum: cefe79e25582b635c5321cf2c091404f (MD5) / A paisagem, enquanto resultado das interações endógenas e exógenas, apresenta características distintas, representando seu contexto geomorfológico e os eventos que a modelaram ao longo do tempo. Tais características individualizam a paisagem em unidades, seja pelo relevo, clima, cobertura vegetal, solos, pelo arranjo estrutural e litologia ou exclusivamente por um desses elementos. Usando o mosaico com dados da missão topográfica SRTM que recobrem a Ecorregião do Planalto Central foi realizada 1) a delimitação automática das bacias hidrográficas do Rio das Almas (GO) e Rio Maranhão (GO/DF); e 2) foram extraídas as variáveis morfométricas de declividade, curvatura mínima e máxima e aspecto. As bacias hidrográficas ocupam juntas uma área de 34.641,95 km², correspondem a cerca de 10% da área do Estado do Goiás e possuem litologia representativa da Ecorregião do Planalto Central. As variáveis morfométricas foram alternadas nos canais RGB para selecionar o arranjo de melhor contraste e como resultado obteve-se a altimetria, declividade e curvatura mínima, respectivamente nos canais RGB. A partir da composição colorida os padrões de cor, textura e forma foram vetorizados em tela, resultando em oito unidades geomorfológicas: 1) Chapadas e Remanescentes (3,17%); 2) Frentes de recuo erosivo (12,39%); 3)Rampas de colúvio I (4,53%); 4) Planalto retocado (31,57%); 5) Depressão interplanáltica (18,69%); 6) Serras (14,35%); 7) Rampas de colúvio II (11,99%); e 8) Depressão Dissecada (3,28%). Foi realizado um estudo em nível de bacias e em nível de unidade geomorfológica com base no uso e cobertura da terra a fim de relacionar a distribuição do uso e cobertura da terra às características topográficas de cada unidade. As bacias possuem áreas com uso e cobertura distintos, sendo predominante a agricultura e a pastagem com 32,44% e 40,29%, respectivamente, na bacia do Rio das Almas (GO) e o cerrado com 48,55% na bacia do Rio Maranhão (GO/DF). A unidade geomorfológica de Chapadas e Remanescentes possui potencial de uso para agricultura e cerrado; as Rampas de colúvio I e II, planalto retocado e depressão dissecada possuem potencial de uso para agricultura, pastagem e cerrado; e as Frentes de recuo erosivo e as serras possuem potencial de uso para floresta e cerrado. ______________________________________________________________________________________________ ABSTRACT / The landscape as a result of endogenous and exogenous interactions, has distinct characteristics, representing its geomorphological context and the events that shaped it over time. Such features individualize the landscape units, or topography, climate, vegetation cover, soil, the structural arrangement and lithology or exclusively by one of these elements. Using the mosaic with SRTM topographic mission of data that cover the Ecoregion of the Central Plateau was conducted 1) automatic delineation of the watershed of the Rio das Almas (GO) and Maranhão River (GO / DF); and 2) were extracted morphometric variables of slope, minimum and maximum curvature and aspect. Watersheds together occupy an area of 34,641.95 square kilometers, corresponding to about 10% of the state of Goiás area and have representative lithology of the Central Plateau Ecoregion. The morphometric variables were alternating in the RGB channels to select the best contrast arrangement, and as a result obtained the altitude, slope and minimum curvature respectively in the RGB channels. From the colorful make the color patterns, texture and shape were vectorized on screen, resulting in eight geomorphological units: 1) Plateus and Remmants (3.17%); 2) fronts of erosive retreat (12.39%); 3) Colluvial Ramps I (4.53%); 4) Retouched Plateu (31.57%); 5) Interplanaltic Depression (18.69%); 6) Ridges (14.35%); 7) Colluvial Ramps II (11.99%); and 8) Dissected Depression (3.28%). A study at the level of basins and level of geomorphological unit based on the use and land cover in order to relate the distribution of land use and land cover to the topographical features of each unit was conducted. The basins have areas with different use and cover, being predominantly agriculture and pasture with 32.44% and 40.29%, respectively, in the Almas River basin (GO) and the savannah with 48.55% in the basin Rio Maranhão (GO / DF). The geomorphological unit Chapadas Remnants and has potential use for agriculture and savanna; the Colluvial RampsI and II, retouched and dissected plateau depression have potential use for agriculture, pasture and cerrado; and the erosive retreat fronts and the mountains have potential use for forest and savanna.

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2009. / Submitted by Marília Freitas (marilia@bce.unb.br) on 2011-05-04T19:47:15Z No. of bitstreams: 1 2009_AndreiaBorgesAvelar.pdf: 569913 bytes, checksum: b9c7b5fd67d3f7351a8c69fe64218b4a (MD5) / Approved for entry into archive by Daniel Ribeiro(daniel@bce.unb.br) on 2011-05-07T01:10:24Z (GMT) No. of bitstreams: 1 2009_AndreiaBorgesAvelar.pdf: 569913 bytes, checksum: b9c7b5fd67d3f7351a8c69fe64218b4a (MD5) / Made available in DSpace on 2011-05-07T01:10:24Z (GMT). No. of bitstreams: 1 2009_AndreiaBorgesAvelar.pdf: 569913 bytes, checksum: b9c7b5fd67d3f7351a8c69fe64218b4a (MD5) / Neste trabalho apresenta-se uma formalização do teorema de existência de unificadores mais gerais em teorias de primeira ordem. Tal formalização foi desenvolvida na linguagem de especificação de ordem superior, do assistente de prova PVS. A prova mecânica e muito semelhante as provas encontradas em livros-texto, as quais se baseiam na correção do já conhecido algoritmo de unificação de Robinson de primeira ordem. A prova do teorema foi aplicada dentro de uma teoria completa, desenvolvida em PVS, para sistemas de reescrita de termos, a m de obter uma formalização completa do Teorema dos Pares Críticos de Knuth-Bendix. Para chegar a esta formalização foi construída uma especificação em PVS de uma teoria para unificação de primeira ordem, onde foram formalizadas as propriedades de generalidade e terminação de uma versão do algoritmo de unificação de Robinson restrito a termos unificáveis. _________________________________________________________________________________ ABSTRACT / This work presents the formalization of the theorem of existence of most general unifiers in first-order theories. The formalization was developed in the higher-order speciation language, of the proof assistant PVS. The mechanical proof is very similar to that found in textbooks, which are based on proving the correction of the well-known Robinson's first-order unification algorithm. The proof of the theorem was applied within a complete theory, also developed in PVS, for term rewriting systems in order to obtain the full formalization of the Knuth-Bendix Critical Pair theorem. To reach this formalization, it was build in PVS a specification of a theory first-order unification, where properties of generality and termination of a version of the Robinson's unification algorithm restricted to unifiable terms were formalized.

Made available in DSpace on 2014-06-12T15:58:18Z (GMT). No. of bitstreams: 2 arquivo3452_1.pdf: 3452194 bytes, checksum: f140ad60d48eddac72b254cec44bfe46 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / O advento das novas tecnologias Very Large Scale Integration (VLSI) e o crescimento da demanda por produtos eletrônicos no mundo estão trazendo um aumento explosivo na complexidade dos circuitos eletrônicos. A contrario sensu, o tempo de mercado (time-tomarket) de um produto eletrônico, e o tempo de projeto necessário para produção e venda de um sistema estão ficando cada vez menores. Para que o circuito integrado chegue ao mercado com o funcionamento esperado é necessário realizar testes. Parte desses testes é chamada de verificação funcional e é a parte do projeto que requer mais tempo de desenvolvimento. Buscam-se sempre novos métodos que permitam que a verificação funcional seja realizada de forma ágil, fácil e que proveja uma maior reusabilidade e diminuição da complexidade na construção do ambiente de simulação, sem interferir negativamente na qualidade do processo de verificação e do produto. Dessa forma, o uso de uma metodologia de verificação funcional eficiente e de ferramentas que auxiliem o engenheiro de verificação funcional é de grande valia. A metodologia OVM_tpi permite o desenvolvimento de todo o fluxo de construção de um ambiente de verificação, independente da escolha feita pela equipe desenvolvedora, de forma que o ambiente de simulação seja gerado antes da implementação do circuito a ser verificado (Design Under Verification - DUV). Além disso, ataca os principais desafios do processo de verificação funcional, tempo e custo de desenvolvimento, contribuindo para uma diminuição da complexidade, reusabilidade, comunicação entre o ambiente com uma interface bem definida e diminuição no tempo de desenvolvimento de um testbench através do uso de templates que criam de forma semiautomática partes do ambiente de verificação. OVM_tpi teve como principal base a metodologia Open Verification Methodology (OVM), utilizando sua biblioteca para a construção do testbench e o paradigma de linguagem orientação objeto suportado por SystemVerilog, linguagem criada especialmente para verificação funcional e design. Sua validação foi através de estudos de casos que demonstraram a eficácia do seu uso, tanto para circuitos unidirecionais, quanto para bidirecionais

Made available in DSpace on 2014-06-12T15:59:18Z (GMT). No. of bitstreams: 2 arquivo5011_1.pdf: 1099518 bytes, checksum: 29a36710d81ec239b320f6d900a43fc5 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2004 / Leis de programação são importantes tanto para definir a semântica axiomática de linguagens de programação quanto para auxiliar o processo de desenvolvimento de software. De fato, estas leis podem ser utilizadas como base para práticas informais de desenvolvimento como refactoring, que vem sendo popularizada por metodologias modernas, em especial por Extreme Programming. Embora não tenham sido suficientemente exploradas ainda, as leis de modelagem provavelmente podem trazer benefícios similares, mas com um impacto positivo maior em confiabilidade e produtividade, devido ao melhor suporte antecipado no processo de desenvolvimento de software. Em geral, transformação de modelos que preservam semântica são propostas de maneira ad hoc tendo em vista que são difíceis de serem provadas que são consistentes com respeito a semântica formal. Como consequência, pequenos equívocos podem levar a transformações que deixem o modelo inconsistente. Por estes motivos, este trabalho propõe um conjunto de leis de modelagem (que podem ser vistas como transformações de modelos bidirecionais que preservam semântica) que podem ser utilizas com segurança para se derivar leis mais complexas. Estas leis descrevem transformações de modelos em Alloy, uma linguagem formal para modelagem orientada a objetos. Além disso, será mostrada como estas leis podem ser utilizadas para refatorar especificações em Alloy. Com o intuito de se verificar a consistência das leis, foi proposta uma semântica denotacional para Alloy, utilizando a própria linguagem e uma noção de equivalência indicando quando dois modelos em Alloy possuem a mesma semântica. Por fim, o Alloy Analyzer, ferramenta utilizada para fazer análises em modelos em Alloy, foi estendida com algumas das leis básicas propostas. Como resultado, algumas diretrizes para a implementação de sistemas de transformação foram propostas

Made available in DSpace on 2014-06-12T15:59:45Z (GMT). No. of bitstreams: 2 arquivo5534_1.pdf: 549658 bytes, checksum: 33407312a37208868737b8dacb036de5 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2006 / Uma grande quantidade de estudos relacionados a sistemas on-line de verificação vem sendo conduzida por pesquisadores nos últimos anos. No entanto, investigações a respeito da influência do tamanho das assinaturas no seu processo de formação são escassas. De fato, este tipo de análise para sistemas de verificação on-line está sendo feito pela primeira vez. Nesta dissertação, com o objetivo de investigar esta influência, uma base de dados contendo assinaturas com três tamanhos diferentes foi criada. Os resultados obtidos mostraram que assinaturas de tamanhos diferentes são estatisticamente diferentes e podem influenciar as técnicas de extração de características, o que, por sua vez, influenciam as taxas de acertos dos sistemas de verificação. Portanto, uma atenção especial deve ser tomada na implementação de aplicações globais que utilizam bases de dados com assinaturas de diferentes tamanhos. Nos experimentos realizados, as assinaturas médias, no melhor dos casos, obtiveram um erro médio de classificação de 1,96%, enquanto que as assinaturas pequenas e grandes, após um processo de seleção de característica, obtiveram um erro médio de 4,04% e 4,25% respectivamente. Através de uma seleção local de características, foi possível minimizar a influência dessas distorções causadas pela variação dos tamanhos das assinaturas