Submitted by Lúcia Brandão (lucia.elaine@live.com) on 2015-12-11T18:49:43Z No. of bitstreams: 1 Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-01-19T14:41:05Z (GMT) No. of bitstreams: 1 Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-01-19T14:54:32Z (GMT) No. of bitstreams: 1 Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) / Made available in DSpace on 2016-01-19T14:54:32Z (GMT). No. of bitstreams: 1 Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) Previous issue date: 2015-07-03 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Oneofthemainchallenges insoftwaredevelopment istoensurethesafetyofthesoftwaresystems, especially in critical embedded systems, such as aircraft or healthcare, where several constraints (e.g., response time and data accuracy) must be met and measured in accordance with the user requirements, otherwise a failure can lead to catastrophic situations. Thus, software verification and testing techniques are essential items for the software development with quality, where such techniques aim to confirm the user requirements, as well as, the predetermined behaviors for the software. In the software verification context, aiming the product quality, the formal verification technique called model checking has been used to find subtle errors in actual projects of the software systems. However, the use of the model checking technique presents some challenges such as dealing with the model’s state explosion problem, integration with software testing environments more familiar to designers, and handling counter-examples to reproduce the identified errors. In order to deal with these problems, a possible solution is to explore the characteristics already provided by the model checkers, e.g., verification of the safety properties and generation of counter-examples. Exploring this set of characteristics, coupled with the use of program invariants inference and a special kind of model checking, called Bounded Model Checking (BMC), this thesis presents a set of methods to complement and enhance the scalability and accuracy of the verification performed by Bounded Model Checkers. These methods adopted code transformation techniques to explore the characteristics of Bounded Model Checkers to analyze the safety properties and demonstrate errors in programs written inthe C programming language. The methods presented in this thesis are: (1) The automatic generation and verification of the test cases based on safety properties generated by a Bounded Model Checker for unit tests; (2) Automating thecollection andmanipulation of thedatafrom thecounter-examples, todemonstrate the main cause of the identified error; and (3) Adopting program invariants dynamically/statically inferred from the analyzed program, to restrict the exploration of the states sets while performing the verification by the BMC. This way, helping to improve the verification performed by a BMC, related to assist in the verification and accuracy of results, by adoption of the program invariants. The proposed approaches when used separately, provide additional options to the verification, and interconnected, improving the code verification. Theexperimental results of theproposed methods show to be efficient over public available benchmarks of C programs, finding errors not previously found byother methods that are state-of-the-art. / Um dos principais desafios no desenvolvimento de software é garantir a funcionalidade dos sistemas de software, especialmente em sistemas embarcados críticos, tais como aeronáutico ou hospitalar, onde diversas restrições (por exemplo, tempo de resposta e precisão dos dados) devem ser atendidas e mensuradas de acordo com os requisitos do usuário, caso contrário uma falha pode conduzir a situações catastróficas. Logo, técnicas de verificação e teste de software são itens indispensáveis para um desenvolvimento com qualidade, onde tais técnicas visam confirmar os requisitos do usuário, bem como os comportamentos pré-estabelecidos para osoftware. No contexto de verificação de software, visando à qualidade geral do produto, a técnica de verificação formal model checking tem sido utilizada para descobrir erros sutis em projetos de sistemas de software atuais. Contudo, a utilização da técnica model checking apresenta alguns desafios, tais como, lidar com a explosão do espaço de estados do modelo, integração com outros ambientes de testes mais familiares aos projetistas e tratamento e análise de contra-exemplos para reprodução de erros. De modo a lidar com estes problemas, uma possível solução é explorar as características já providas pelos model checkers, por exemplo, a verificação de propriedades de segurança e geração de contra-exemplos. Explorando este conjunto de características, juntamente com autilização dainferência deinvariantes eumtipo especial demodelchecking, denominado de BoundedModelChecking (BMC),esta tese apresenta um conjunto de métodos para complementar e aprimorar a escalabilidade e acurácia da verificação efetuada por Bounded Model Checkers. Estes métodos utilizam técnicas de transformações de código para explorar as características de Bounded Model Checkers, a fim de analisar propriedades de segurança e demonstrar erros em códigos escritos na linguagem de programação C. Os métodos apresentados nesta tese são: (1) A geração e verificação automática de casos de teste baseado em propriedades de segurança geradas por um Bounded Model Checker para testes de unidade; (2) Automatizar acoleta emanipulação das informações dos contra-exemplos, de modo a demonstrar a causa principal do erro identificado; e (3) Utilização de invariantes dinamicamente/estaticamente inferidas, a partir do programa analisado, para restringir a exploração dos conjuntos de estados durante a execução da verificação pelo BMC. Desta forma, ajudando no aprimoramento da verificação efetuada por um BMC, no que concerne em auxiliar a sua verificação e na precisão dos resultados, pela utilização de invariantes de programas. As abordagens propostas, quando utilizadas isoladamente, fornecem alternativas complementares a verificação e, interligadas, aprimoram a verificação de código. Os resultados experimentais dos métodos propostos demonstram ser eficientes sobre benchmarks públicos de programas em C, encontrando defeitos não anteriormente encontrados por outros métodos que são estado-da-arte.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:38Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:50Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Made available in DSpace on 2018-03-21T17:40:50Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) Previous issue date: 2017-08-10 / FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas / The use of embedded systems, i.e., computer systems focused on performing specific functions in larger (electronic or mechanical) systems, has been growing lately, and ensuring the robustness of such systems has become increasingly important. There are several techniques to ensure that a system is released without errors. In particular, formal verification of programs is proving itself to be effective in the search for failures. In this work, an induction-proof algorithm is described, which combines k-induction and invariants to verify and refute safety properties in embedded ANSI-C software. Moreover, the proposed k-induction-based approach infers invariants in the program to assist in verification tasks, using constraint refinement (i.e., polyhedral) to specify pre- and post-conditions. We adopted two invariant generators to produce such and feed the k-induction algorithm, which is implemented in the Efficient SMT-Based Context-Bounded Model Checker tool. Public benchmarks were used to assess the effectiveness of our approach. In addition, a comparison to other state-of-the-art verification tools using a set of benchmarks from the International Competition for Software Verification in addition to embedded systems applications. Experimental results have shown that the proposed approach, with and without invariants, can verify a wide variety of safety properties in programs with loops and embedded software from telecommunications, control systems, and medical domains. / O uso de sistemas embarcados, sistemas computacionais especializados para execução em sistemas eletrônicos ou mecânicos tem crescido de forma vertiginosa devido a utilização cada vez mais intensa de sensores, interfaces de rede e protocolos de comunicação em diversas áreas. Por isso, é cada vez mais importante garantir a robustez desses sistemas, uma vez que estão se tornando mais complexos e integrados. Existem várias técnicas para garantir que um sistema seja entregue ao cliente sem erros, em particular, a verificação formal dos programas tem se revelado eficaz na busca de falhas. Neste trabalho é descrito um algoritmo de indução matemática conhecido como k-induction combinado ao uso de invariantes para verificar e refutar propriedades de segurança em programas desenvolvidos na linguagem ANSI-C. Em particular, a abordagem proposta infere invariantes no programa para auxiliar na verificação de programas ANSI-C através da técnica de indução matemática através do refinamento de restrição (i.e, poliédrico) para especificar pré- e pós-condições. No método proposto, adotamos dois geradores de invariantes para produzir e alimentar o algoritmo de indução matemática o qual é implementado na ferramenta Efficient SMT-Based Context-Bounded Model Checker. A motivação para a combinação de invariantes com o algoritmo de indução matemática é fechar um gap na verificação formal de programas que possuam variáveis globais, além de programas com loops que possuem desvios condicionais e o número de iterações é desconhecido. PIPS e PAGAI são as ferramentas utilizadas para analisar o código e produzir invariantes indutivas responsáveis por guiar o algoritmo de indução matemática na verificação do benchmark, sendo este o principal desafio do método proposto. Para avaliar a eficácia da abordagem proposta neste trabalho, além de aplicações de Sistemas Embarcados foram utilizados benchmarks públicos disponibilizados pela Competição Internacional de Verificação de Software onde participam Universidades, pesquisadores, estudandantes de doutorado de várias partes do mundo, e fornece amplo conjunto de casos de teste para verificação. Além disso, foram utilizadas ferramentas estado-da-arte para a comparação dos resultados e, assim mensurar a eficácia do método proposto. Os resultados experimentais foram positivos e mostraram que o algoritmo de indução matemática com invariantes pode verificar uma grande variedade de propriedades de segurança em programas com loops e aplicações de sistemas embarcados de telecomunicações, sistemas de controle e dispositivos médicos.

A geometria de teias dedica-se ao estudo de invariantes locais para uma determinada configuração de folheações. Uma d-teia é uma coleção de folheações que estão em posição geral. Desta forma, uma d-teia plana, definida em \'R POT.2\' ou \'C POT.2\', nada mais é que uma família de d folheações por curvas. Apresentamos neste trabalho os principais conceitos da teoria clássica de teias, iniciada por W. Blaschke por volta de 1930, bem como uma abordagem atual utilizada no estudo de teias planas. São abordados dois tipos de problemas importantes na teoria: os problemas de linearização e de algebrização de teias. Provamos um resultado clássico no que concerne ao problema de linearização, e um resultado de algebrização de teias empregando métodos desenvolvidos mais recentemente / Web geometry is devoted to the study of local invariants of a certain configuration of foliations. A d-web is a collection of foliations in general position. Therefore, a d-web defined in \'R POT. 2\' or \'C POT. 2\' is just a family of d foliations by curves. We present in this work the main concepts of classical theory of webs, initiated by W. Blaschke around 1930, as well as newer methods used in the study of plane webs. We approach two important types of problems in the theory: problems of linearization and that of algebrization of webs. We prove a classical result concerning the linearization problem, and a result of algebrization of webs using recently developed methods

Neste trabalho obtemos que o espaço dos invariantes locais do tipo Vassiliev de primeira ordem de aplicações estáveis de 3-variedade fechada orientada em \' R POT. 4\' é 4-dimensional. Damos uma interpretação geométrica para 2 dos 4 geradores deste espaço, a saber, \'I IND. Q\' o número de pontos quádruplos e \'I IND. C / P\' o número de pares de pontos do tipo crosscap/plano, da imagem de uma aplicação estável. Ao reduzir o espaço das aplicações para o das imersões esáaveis, obtemos que o espaço dos invariantes locais de imersões estáveis é 3-dimensional. Os invariantes que obtemos são: \'I IND. Q\' o número de pares de pontos quádruplos da imagem de uma imersão estável e dois índices de interseção \'I IND. I\'`+ e \'I IND. l\' introduzidos por V. Goryunov em [15]. Como início de um estudo que almejamos realizar sobre a geometria de uma m-variedade em \'R POT. m+1\' com singularidades, obtemos os tipos de contatos genéricos da suspensão do crosscap (única singularidade estavel de \'R POT. 3\' em \'R POT. 4\' ) com hiperplanos de \'R POT.4\' / In this work we obtain that the space of first order local Vassiliev type invariants of stable maps of oriented 3-manifolds in \'R POT. 4\' is 4-dimensional. We give a geometric interpretation for two of the four generators of this space, namely, \'I IND. Q\' the number of quadruple points and \'I IND. C / P\' the number of pairs of points of crosscap/plane type, of the image of a stable map. In the case of stable immersions, we obtain that the space of local invariants of stable immersions is 3-dimensional. The invariants that we obtain are: \'I IND. Q\' the number of pairs of quadruple points of the image of a stable immersion and the positive and negative linking invariants \'I IND. I`+ and I\'I IND., l\' introduced by V. Goryunov in [15]. As a beging of a study that we want to realise about the geometry of a m-manifold in \'R POT. m+1\' with singularities, we obtain the generic contacts of the suspension of crosscap (the only stable singularity from \'R POT. 3\' to \'R POT. 4\') with hyperplanes of \'R POT. 4\'

Orientador: Dessislava Hristova Kochloukova / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matemática Estatística e Computação Científica / Made available in DSpace on 2018-08-23T11:19:15Z (GMT). No. of bitstreams: 1 Lima_FrancismarFerreira_M.pdf: 2264816 bytes, checksum: 31f3b411247775dcde6338655fbd496b (MD5) Previous issue date: 2013 / Resumo: O resumo poderá ser visualizado no texto completo da tese digital / Abstract: The complete Abstract is available with the full electronic document. / Mestrado / Matematica / Mestre em Matemática

Orientador: Dessislava Hristova Kochloukova / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Matemática, Estatística e Computação Científica / Made available in DSpace on 2018-08-20T20:07:55Z (GMT). No. of bitstreams: 1 Almeida_KisnneyEmilianode_D.pdf: 833428 bytes, checksum: 3f425f5150e4ce7915c42d59f2a772be (MD5) Previous issue date: 2012 / Resumo: A teoria de ?-invariantes surgiu do trabalho de Bieri e Strebel, que definiram o primeiro ?-invariante, apenas para grupos metabelianos, e o usaram para descrever os grupos metabelianos finitamente gerados [BiSt]. Posteriormente, foram definidos os ?m-invariantes homotópicos e homológicos de grupos finitamente gerados arbitrários [BiNSt]. Estes são certos subconjuntos da esfera de caracteres profundamente relacionados às propriedades de finitude Fm e FPm, respectivamente. Os grupos de Artin formam uma grande classe de grupos, cada um associado a um grafo rotulado, que inclui algumas subclasses importantes, como "Braid groups" e "Rightangled Artin groups"...Observação: O resumo, na íntegra, poderá ser visualizado no texto completo da tese digital / Abstract: The ?-invariants theory arose from the work of Bieri and Strebel, who defined the first ?-invariant, for metabelian groups only, and used it to describe the finitely presented metabelian groups [BiSt]. Later on, the homotopical and homological ?m-invariants of arbitrary finitely generated groups were defined [BiRe]. These are certain subsets of the sphere of characters deeply related to the finiteness properties Fm and FPm, respectively. The Artin groups form a large class of groups, each one associated to a labeled graph, that includes some important subclasses, as Braid groups and Right-angled Artin groups...Note: The complete abstract is available with the full electronic document / Doutorado / Matematica / Doutor em Matemática

Orientador : Amauri Lopes / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-08-01T04:43:21Z (GMT). No. of bitstreams: 1 Boaventura_WallacedoCouto_D.pdf: 1878823 bytes, checksum: 97df3e94f4b5c7c7211ba0ed14e6de34 (MD5) Previous issue date: 2002 / Doutorado

Orientador: Yuri Dimitrov Bozhkov / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Computação Cientifica / Made available in DSpace on 2018-08-02T18:57:52Z (GMT). No. of bitstreams: 1 Martins_AntonioCarlosGilli_D.pdf: 481173 bytes, checksum: 10a4c4f008edd1971b53b1c64423a6e5 (MD5) Previous issue date: 2002 / Doutorado / Doutor em Matemática

Orientador: João Mauricio Rosario / Tese (doutorado) - Univesidade Estadual de Campinas, Faculdade de Engenharia Mecanica / Made available in DSpace on 2018-08-03T16:34:10Z (GMT). No. of bitstreams: 1 Oliveira_Clivaldode_D.pdf: 5223998 bytes, checksum: c36fcec78e3e356ae03181c517e79e0a (MD5) Previous issue date: 2003 / Resumo: Este trabalho tem como objetivo a modelagem e simulação de sistemas dinâmicos, com ênfase no estudo e implementação de controladores de posição de juntas robóticas. Inicialmente é realizado o estudo dos elementos constituintes de uma junta robótica, tais como: motor de corrente contínua, inércia, redutores e acoplamento. A partir desse estudo é possível a definição da estratégia de controle a ser utilizada, incluindo o desenvolvimento de um gerador de trajetórias utilizado como referencia dentro de uma malha de controle envolvendo estes elementos. A validação final dos algoritmos de controle desenvolvidos é realizada através de uma bancada experimental descrita nesse trabalho / Abstract: This work has as objective the modeling and simulation of dynamic systems, with emphasis in the study and controllers of position of joints robotics implementation. Initially the study of the constituent elements ofajoint robotics is accomplished, such as: DC motor, inertia and reducers. To go on with this study will be necessary the definition of the control strategy, inc1uding the development of a generator of trajectories used inside as reference of a control involving these elements. The final validation of the developed control algorithms is accomplished through a supported experimental / Doutorado / Mecanica dos Sólidos e Projeto Mecanico / Doutor em Engenharia Mecânica

[pt] Este trabalho aborda o problema da estabilidade de sistemas lineares, invariantes no tempo, a tempo discreto, com o espaço de estado sendo um espaço de Hilbert complexo e separável de dimensão infinita. São investigadas condições necessárias e/ou suficientes para quatro conceitos diferentes de estabilidade: estabilidade assintótica uniforme e estabilidade assintótica forte, estabilidade assintótica fraca e estabilidade limitada. Identifica-se e analisa-se as conexões entre os problemas de estabilidade e dois problemas em aberto da teoria de operadores em espaços de Hilbert: o problema do subespaço invariante e o problemas da similaridade e contração. Diversos resultados, oriundos de tentativas de solução para os dois problemas acima, ou motivados por aquelas tentativas, são utilizadas para fornecer caracterizações adicionais (principalmente caracterizações espectrais) para os quatro conceitos de estabilidade em questão. / [en] This work deals with the stability problem for time- invariant discrete linear systems evolving in a separable infinite-dimensional Hilbert space. Necessary and/or sufficient conditions for uniform, strong and weak asymptotic stability, as well as to bounded stability problems to two open problems in operator theory, namely, the invariant subspace and the similarity to contractions, are identified and analysed in detail. Several results from the many attempts, of solving the above mentioned open problems, or motivated by those attempts, are used to supply additional characterizations (mainly spectral characterization) for the four stabilty concepts under consideration.