Submitted by Algacilda Conceição (algacilda@sibi.ufrj.br) on 2018-04-02T14:41:15Z No. of bitstreams: 1 133291.pdf: 2852001 bytes, checksum: d16e2ebe65998bf843ce0c848d5f5b94 (MD5) / Made available in DSpace on 2018-04-02T14:41:15Z (GMT). No. of bitstreams: 1 133291.pdf: 2852001 bytes, checksum: d16e2ebe65998bf843ce0c848d5f5b94 (MD5) Previous issue date: 1973-08 / CAPES / Universidade Federal de Pernambuco / Estuda sobre estabilidade de redes RC não lineares. Uma rede RC é considerada assintóticamente estável quando a carga dos capacitores converge a uma carga de equilíbrio. O estudo é desenvolvido a partir da análise do comportamento de redes resistivas. Em todo trabalho é admitida a hipótese dos resistores possuírem curvas características crescentes, com o que, formular os problemas de redes resistivas como problemas de otimização em grafos. Técnicas de dualidade são utilizadas na dedução de alguns resultados. Hipóteses adicionais sobre os resistores, dependentes da estrutura da rede, permitirão representar-se as soluções de rede como soluções de um sistema de equações diferenciais onde a existência e unicidade de soluções é garantida. O método de Liapunov é o instrumento básico na análise de estabilidade deste sistema de equações. / Study of non-linear RC network stability. An RC network is considered assymptotically stable when the capacitar charges converge to equilibrium charges. The study is developed from the analysis of the behavior of resistive networks. It is assumed that all resistors have increasing characteristics curves, from which it is possible to formulate resistive network problems as optimization problems on graphs. Duality techniques are used in the proof of certain results. Additional hypothesis on the resistors, depending on the network structure, will permit representation of the networks solutions as solutions of a system of differential equations for which the existence and uniqueness of solutions is guaranteed. Liapunov's method is the basic tool in the stability analysis of this system of equations.

Submitted by Algacilda Conceição (algacilda@sibi.ufrj.br) on 2018-04-03T16:33:27Z No. of bitstreams: 1 132130.pdf: 2222697 bytes, checksum: 1ec12d8948f550cbe0e268b315624644 (MD5) / Made available in DSpace on 2018-04-03T16:33:27Z (GMT). No. of bitstreams: 1 132130.pdf: 2222697 bytes, checksum: 1ec12d8948f550cbe0e268b315624644 (MD5) Previous issue date: 1973-03 / Estudo de sistemas de controle ótimo, discretos no tempo, nos quais o controle é restringido pelo estado do sistema. Inicialmente é feito um desenvolvimento rigoroso de condições necessárias e suficientes que devem ser satisfeitas pela solução ótima, usando-se para isto métodos de programação dinâmica. Em seguida é apresentado o “princípio do máximo” discreto dado por Cannon, Cullum e Polak [6]. Exemplos são dados, mostrando que o “princípio do máximo” usual não é satisfeito para problemas com controles restringidos pelo estado. É formulada então uma “hipótese de inclusão” mostrando uma classe de problemas que satisfazem o “princípio do máximo” usual. Por último teorema de Fritz-John é aplicado para obter condições necessárias para problemas com restrições da forma R(x, u) ≤ 0 e um “princípio do máximo modificado” é apresentado. É mostrado ainda que sistemas lineares positivos, frequentemente encontrados em economia, satisfazem o “princípio do máximo modificado”. Vários exemplos resolvidos em detalhe ilustram o texto. / Study of discrete optimal control problems in which the control is restricted by the state of the system. Initially, a rigorous self contained developnent of necessary and sufficient conditions is given through dynamic programming. This is followed by a developnent of the discrete maximum principle, presented in the manner of Cannon, Cullum and Polak. [6]. Examples are given to show that the maximurn principle usually does not hold in the case of state constrained controls and an "inclusion hypotheses" is given, demonstrating a class of problems where the usual maximum principle is valid. The Fritz John Theorem is then applied to obtain necessary conditions for problems with oonstraints of the form R(x,u) ≤ 0 and a modified maximurn principle is defined for this class. It is shown that linear positive systems of a type frequently encountered in economic systems satisfy the modified maximum principle. A number of detailed examples are given throug out the text.

Submitted by Algacilda Conceição (algacilda@sibi.ufrj.br) on 2018-04-05T18:42:01Z No. of bitstreams: 1 131488.pdf: 3589192 bytes, checksum: 5c39ddf4ef3d285ba2bccd969b191920 (MD5) / Made available in DSpace on 2018-04-05T18:42:01Z (GMT). No. of bitstreams: 1 131488.pdf: 3589192 bytes, checksum: 5c39ddf4ef3d285ba2bccd969b191920 (MD5) Previous issue date: 1973-01 / Usa a informação sintática contida nas sentenças pertencentes a uma linguagem formal na sua decodificação quando as mesmas são transmitidas através um canal ruidoso. É adaptado o algoritmo de Fano da decodificação sequencial na decodificação sintática. O algoritmo é simulado em computador IBM 370 para três diferentes linguagens e canais de transmissão. / Use the syntactical information of the sentences of a formal language in their decoding, after they have passed through a noisy channel. Fano's algorithm for sequential decoding is adapted to syntactical decoding. The algorithm is simulated in the IBM 370 for three diferent sources and channels. The results o f the simulation are discussed and analysed.

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-08-26T23:09:02Z No. of bitstreams: 1 IngridMorganeMedeirosDeLucena_DISSERT.pdf: 1893477 bytes, checksum: af3baeea1aaa51a500a23196c3ed264b (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-08-30T23:12:54Z (GMT) No. of bitstreams: 1 IngridMorganeMedeirosDeLucena_DISSERT.pdf: 1893477 bytes, checksum: af3baeea1aaa51a500a23196c3ed264b (MD5) / Made available in DSpace on 2016-08-30T23:12:54Z (GMT). No. of bitstreams: 1 IngridMorganeMedeirosDeLucena_DISSERT.pdf: 1893477 bytes, checksum: af3baeea1aaa51a500a23196c3ed264b (MD5) Previous issue date: 2016-02-03 / A ?rea denominada de Engenharia de Software Baseada em Pesquisa (Search Based Software Engineering) vem crescendo nas ?ltimas d?cadas e possui um grande n?mero de trabalhos dedicados a ela. Esta ?rea re?ne a Engenharia de Software e a Otimiza??o no desenvolvimento de algoritmos que otimizem os custos de atividades inerentes ao processo do desenvolvimento de software. Dentre tais atividades est? o teste de software, o qual visa verificar, detectar e corrigir poss?veis erros cometidos pelos programadores. Uma vez que esta atividade ? respons?vel por at? 50% do custo total do desenvolvimento, os pesquisadores buscam minimizar o custo dos testes sem comprometer a qualidade do software. Os primeiros trabalhos abordando atividades de Teste de Software como problemas de otimiza??o surgiram na d?cada de 70. Este trabalho tem por objetivo realizar uma revis?o do estado-da-arte das t?cnicas e algoritmos de otimiza??o desenvolvidos para teste de software, estendendo um trabalho anterior, com a revis?o de 415 artigos da ?rea. ?, tamb?m, apresentada uma classifica??o de tais trabalhos quanto aos tipos de m?tricas, algoritmos de otimiza??o e outras caracter?sticas dos problemas inerentes ao teste de software. / The area known as Search Based Software Engineering has been growing in recent decades and has a large number of works dedicated to it. This area gathers the Software Engineering and Optimization in the development of algorithms that optimize the costs of activities related to the software development process. Software testing is one among those activities which aims at checking, detecting and correcting possible errors made by programmers. Since this activity is responsible for 50% of the total development cost, researchers seek to minimize testing costs without compromising the software quality. Early works addressing Software Testing activities as optimization problems arose in the 70s. This paper aims to conduct a review of the state of the art techniques and optimization algorithms developed for a major problem area, the Test Data Generation problem. A classification of works by metrics, optimization algorithms and other characteristics inherent to software testing problem.

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-08-26T23:09:02Z No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-08-30T23:32:12Z (GMT) No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) / Made available in DSpace on 2016-08-30T23:32:12Z (GMT). No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) Previous issue date: 2016-04-29 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior (CAPES) / A presente disserta??o descreve uma extens?o para a plataforma Frama-C e o plugin WP:o WPTrans. Essa extens?o permite a manipula??o, atrav?s de regras de infer?ncia, dasobriga??es de prova geradas pelo WP, com a possibilidade das mesmas serem enviadas,em qualquer etapa da modifica??o, a solucionadores SMT e assistentes de prova. Algumasobriga??es de prova podem ser validadas automaticamente, enquanto outras s?o muitocomplexas para os solucionadores SMT, exigindo uma prova manual pelo desenvolvedor,atrav?s dos assistentes de prova. Contudo, a segunda abordagem geralmente requer dousu?rio uma experi?ncia significativa em estrat?gias de prova. Alguns assistentes oferecemcomunica??o com provadores autom?ticos, entretanto, esta liga??o pode ser complexaou incompleta, restando ao usu?rio apenas a prova manual. O objetivo deste plugin ? interligaros dois tipos de ferramentas de modo preciso e completo, com uma linguagemsimples para a manipula??o. Assim, o usu?rio pode simplificar suficientemente as obriga??es deprova para que possam ser validadas por qualquer outro solucionador SMT.N?o obstante, a extens?o ? interligada diretamente ao WP, facilitando a instala??o doplugin no Frama-C. Esta extens?o tamb?m ? uma porta de entrada para outras poss?veisfuncionalidades, sendo as mesmas discutidas neste documento. / The platform Frama-C is a tool dedicated to analysis of source code of software written in C, with the possible types of analysis provided by plugins attached to the platform. One of its plugins is WP, used for deductive veri cation of C code with ACSL, a formal speci cation language. This dissertation describes the extension of this plugin, named WPTrans. This extension allows generated proof obligations from WP to be manipulated through inference rules and sent, at any stage of the proof, to automatic (mainly SMT solvers) and interactive theorem provers. Some proof obligations may be proved automatically, while others can be too complex to be solved by automatic theorem provers, requiring the users of Frama-C and WP to handle them manually. This approach usually requires a signi cant experience in proof strategies. Some interactive theorem provers provide communication with automatic provers. However, this connection can be complex and incomplete, leaving the user with the manual proof option only. The strength of WPTrans is to combine the features of automatic and interactive theorem provers in a precise and complete way, with a simple manipulation language. Thus, the user can simplify the proof obligations enough in order for its proof to be concluded with an SMT solver, letting the proof be partially manual and partially automatic. Nevertheless, the plugin is directly linked do WP, facilitating the installation of the extension in Frama-C. This tool is also a gateway to other possible features, which we discuss herein.

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-10-11T20:48:07Z No. of bitstreams: 1 ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-10-14T00:17:49Z (GMT) No. of bitstreams: 1 ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) / Made available in DSpace on 2016-10-14T00:17:49Z (GMT). No. of bitstreams: 1 ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) Previous issue date: 2016-04-14 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior (CAPES) / Sistemas de software esta?o presentes em grande parte das nossas vidas atualmente e, mais do que nunca, eles requerem um alto ni?vel de confiabilidade. Existem va?rias te?cnicas de Ver- ificac?a?o e Validac?a?o (V&V) de software que se preocupam com controle de qualidade, segu- ranc?a, robustez e confiabilidade; as mais conhecidas sa?o Testes de Software e Me?todos For- mais. Me?todos formais e testes sa?o te?cnicas que podem se complementar. Enquanto me?to- dos formais prove?em mecanismos confia?veis para raciocinar sobre o sistema em um ni?vel mais abstrato, te?cnicas de teste ainda sa?o necessa?rias para uma validac?a?o mais profunda e sa?o frenquentemente requeridas por orga?os de certificac?a?o. Levando isto em considerac?a?o, BETA prove? uma abordagem de testes baseada em modelos para o Me?todo B, suportada por uma ferramenta, que e? capaz de gerar testes de unidade a partir de ma?quinas abstratas B. Nesta tese de doutorado apresentamos melhorias realizadas em BETA e novos estudos de caso realizados para avalia?-la. Dentre as melhorias, integramos crite?rios de cobertura lo?gicos a? abordagem, revisamos os crite?rios de cobertura baseados em espac?o de entrada que ja? eram suportados e aperfeic?oamos as u?ltimas etapas do processo de gerac?a?o de testes. A abordagem agora suporta a gerac?a?o automa?tica de dados para os ora?culos e prea?mbulos para os casos de teste; ela tambe?m possui uma funcionalidade para concretizac?a?o dos da- dos de teste e um mo?dulo para gerar scripts de teste executa?veis automaticamente. Outro objetivo desta tese foi realizar estudos de caso mais complexos utilizando BETA e avaliar a qualidade dos casos de teste que a abordagem produz. Estes estudos de caso foram os primeiros a avaliar o processo de gerac?a?o de testes por completo, desde a especificac?a?o dos casos de teste ate? a sua implementac?a?o e execuc?a?o. Em nossos u?ltimos experimentos, analisamos a qualidade dos casos de teste gerados por BETA, considerando cada crite?rio de cobertura suportado, utilizando me?tricas de cobertuda de co?digo como cobertura de in- struc?o?es e ramificac?o?es. Tambe?m utilizamos testes de mutac?a?o para avaliar a capacidade dos casos de teste de detectar faltas na implementac?a?o dos modelos. O resultados obtidos foram promissores mostrando que BETA e? capaz de detectar faltas introduzidas por progra- madores ou geradores de co?digo e que a abordagem pode obter bons resultados de cobertura para a implementac?a?o de um sistema baseado em modelos B. / Software systems are a big part of our lives and, more than ever, they require a high level of reliability. There are many software Verification and Validation (V&V) techniques that are concerned with quality control, security, robustness, and reliability; the most widely known are Software Testing and Formal Methods. Formal methods and testing are techniques that can complement each other. While formal methods provide sound mechanisms to reason about the system at a more abstract level, testing techniques are still necessary for a more in-depth validation of the system and are often required by certification standards. Taking this into consideration, BETA provides a tool-supported, model-based testing approach for the B Method that is capable of generating unit tests from abstract B machines. In this thesis, we present improvements made in the BETA approach and tool, and new cases studies used to evaluate them. Among these improvements, we integrated logical coverage criteria into the approach, reviewed the input space criteria that was already supported, and enhanced the final steps of the test generation process. The approach now has support for automatic generation of oracle data and test case preambles, it has a feature for test data concretization, and a module that automatically generates executable test scripts. Another objective of this thesis was to perform more complex case studies using BETA and assess the quality of the test cases it produces. These case studies were the first to evaluate the test generation process as a whole, from test case design to implementation and execution. In our last experiments, we assessed the quality of the test cases generated by BETA, considering each coverage criteria it supports, using code coverage metrics such as statement and branch coverage. We also used mutation testing to evaluate the ability of the generated test cases to identify faults in the model?s implementation. The results obtained were promising, showing that BETA is capable of detecting faults introduced by a programmer or code generation tool and that it can achieve good coverage results for a system?s implementation based on a B model.

Submitted by Fernando Castro (f.h.c.mat010@gmail.com) on 2018-04-24T02:06:10Z No. of bitstreams: 3 Dissertação.pdf: 3513724 bytes, checksum: 30a70d42d3261056f5f5da2b50f69ec2 (MD5) Aprovação.pdf: 10878 bytes, checksum: f562a7550ae34703b803e3d9a83217aa (MD5) carta-comprovanteLOGOdosPPGs.pdf: 216303 bytes, checksum: 646b1697db249ef1a3e646f6da9f4eb6 (MD5) / Approved for entry into archive by Eunice Nunes (eunicenunes6@gmail.com) on 2018-05-07T13:32:51Z (GMT) No. of bitstreams: 3 Dissertação.pdf: 3513724 bytes, checksum: 30a70d42d3261056f5f5da2b50f69ec2 (MD5) Aprovação.pdf: 10878 bytes, checksum: f562a7550ae34703b803e3d9a83217aa (MD5) carta-comprovanteLOGOdosPPGs.pdf: 216303 bytes, checksum: 646b1697db249ef1a3e646f6da9f4eb6 (MD5) / Rejected by Eunice Nunes (eunicenunes6@gmail.com), reason: Boa tarde Fernando, Por favor nos envie sua dissertação com a folha de aprovação já inserida nela. Também verificamos que há várias marcações de hiperlink no texto deixando-o esteticamente não de acordo com as normas e como seu trabalho vai estar disponível em bases nacionais e internacionais recomendo que modifique e envie um novo arquivo com as retificações Fico no aguardo para finalizarmos o processo Qualquer dúvida estou à disposição Obrigada Abraços Eunice on 2018-05-07T13:58:47Z (GMT) / Submitted by Fernando Castro (f.h.c.mat010@gmail.com) on 2018-05-07T14:41:06Z No. of bitstreams: 2 carta-comprovanteLOGOdosPPGs.pdf: 216303 bytes, checksum: 646b1697db249ef1a3e646f6da9f4eb6 (MD5) Dissertação - Fernando Castro.pdf: 3394716 bytes, checksum: d0f4565b103b0d841ebe532ca9d3ce1e (MD5) / Rejected by Ronildo Prado (ri.bco@ufscar.br), reason: Oi Fernando, Faltou inserir a folha de aprovação na dissertação ou tese. Fico no aguardo para finalizarmos o processo. Abraços Ronildo on 2018-05-15T20:12:24Z (GMT) / Submitted by Fernando Castro (f.h.c.mat010@gmail.com) on 2018-05-17T13:52:42Z No. of bitstreams: 2 carta-comprovanteLOGOdosPPGs.pdf: 216303 bytes, checksum: 646b1697db249ef1a3e646f6da9f4eb6 (MD5) Dissertação - Fernando Castro.pdf: 3394716 bytes, checksum: d0f4565b103b0d841ebe532ca9d3ce1e (MD5) / Approved for entry into archive by Ronildo Prado (ri.bco@ufscar.br) on 2018-05-17T18:15:47Z (GMT) No. of bitstreams: 2 carta-comprovanteLOGOdosPPGs.pdf: 216303 bytes, checksum: 646b1697db249ef1a3e646f6da9f4eb6 (MD5) Dissertação - Fernando Castro.pdf: 3394716 bytes, checksum: d0f4565b103b0d841ebe532ca9d3ce1e (MD5) / Approved for entry into archive by Ronildo Prado (ri.bco@ufscar.br) on 2018-05-17T18:15:56Z (GMT) No. of bitstreams: 2 carta-comprovanteLOGOdosPPGs.pdf: 216303 bytes, checksum: 646b1697db249ef1a3e646f6da9f4eb6 (MD5) Dissertação - Fernando Castro.pdf: 3394716 bytes, checksum: d0f4565b103b0d841ebe532ca9d3ce1e (MD5) / Made available in DSpace on 2018-05-17T18:22:05Z (GMT). No. of bitstreams: 2 carta-comprovanteLOGOdosPPGs.pdf: 216303 bytes, checksum: 646b1697db249ef1a3e646f6da9f4eb6 (MD5) Dissertação - Fernando Castro.pdf: 3394716 bytes, checksum: d0f4565b103b0d841ebe532ca9d3ce1e (MD5) Previous issue date: 2018-02-26 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / Climate change is a global issue aggravated by the accumulation of carbon (C) in the atmosphere due to anthropogenic actions. Since the discovery of fossil fuel, its burning has been the main emitter of C to the atmosphere, contributing to raise of Earth's temperature. There are also other sources of C emissions with significant participation in climate change, such as land use change. For centuries, deforestation, burning and poor soil management in the agricultural system have led to a significant loss of forest biomass and soil organic matter, releasing C into the atmosphere in the form of carbon dioxide CO_2, methane CH_4, among other greenhouse gases. Computational models for soil carbon balance were created to evaluate the effect of conventional and conservationist management practices on soil C reservoir. However, most of these models were developed for climate and soil conditions in temperate regions, thus requiring adaptations to Brazilian soil and climate conditions. The objective of this work is to adapt the CQESTR model in a more robust and modern programming language, making its use available for the most current operational systems, Linux and Mac OS, besides Windows. This model was chosen because of its accuracy, simplicity and the need for few input parameters, besides allowing to simulate carbon stocks in the soil at a depth of 3 m. The updated model, in the Python language, was developed by applying object oriented programming techniques. In order to evaluate the new structure of the model, data were used from the systems: no-tillage and conventional tillage with disc plowing, heavy harrowing and scarification, on wheat and soybean crop rotation in the experimental field of Embrapa Soybean in Londrina/PR. The results of the Python model presented similarities to those of the original model, although inaccuracies were found in the second, such as the change in thermal time for simulations with double agricultural rotation per year and the lack of one day in the leap year. The update allows to simulate more than two crops per year, along with leap year implementation in decomposition processes. It also allows to read data from .xlsx and .xls files, making this procedure more agile and easy for the user compared to the original program. The web interface modernized the use of the model, allowing its use in any operational system. The interface in Python will facilitate future updates to the CQESTR model. / As mudanças climáticas são uma questão global que se agrava cada vez mais com o acúmulo de carbono (C) na atmosfera, devido às diversas ações antropogênicas. Desde a descoberta do combustível fóssil, sua queima tem sido o principal emissor de C para a atmosfera, contribuindo para o aumento da temperatura da Terra. Há ainda outras fontes de emissão de C com participações significativas nas mudanças climáticas, como a mudança no uso de terras. Durante séculos, desflorestamento, queimadas e o mau gerenciamento do solo, no sistema agrícola, levaram a uma perda significativa da biomassa das florestas e da matéria orgânica do solo, liberando C para a atmosfera na forma de dióxido de carbono CO_2, metano CH_4, entre outros gases do efeito estufa. Modelos computacionais para o balanço de carbono do solo foram criados para avaliar o efeito de práticas de manejo, convencionais e conservacionista no reservatório de C do solo. Contudo, a maior parte desses modelos foram desenvolvidos para condições de clima e de solo de regiões temperadas, exigindo, portanto adaptações para as condições de clima e solo brasileiros. O objetivo deste trabalho é adaptar o modelo CQESTR em uma linguagem de programação mais robusta e moderna, disponibilizando seu uso para os sistemas operacionais atuais, Linux e Mac OS, além do Windows. Esse modelo foi escolhido por sua acurácia, simplicidade e necessidade de poucos parâmetros de entrada, além de permitir simular estoques de carbono no solo à uma profundidade de até 3 m. O modelo convertido, na linguagem Python, foi desenvolvido aplicando técnicas da programação orientada a objetos. Para avaliar a nova interface do modelo, foram utilizados dados dos sistemas de plantio direto e preparo convencional com arado de disco, gradagem pesada e escarificação, na rotação de trigo e soja, cultivados no campo experimental da Embrapa Soja em Londrina/PR. Os resultados do modelo em Python apresentaram similaridades aos do modelo CQESTR, embora tenham sido encontradas imprecisões no programa original, como a mudança no tempo termal para simulações com rotatividade agrícola no ano e a falta de um dia no ano bissexto. A atualização permite simular mais de duas culturas ao ano, juntamente com a implementação do ano bissexto nos processos da decomposição. Também possibilitou a leitura de dados a partir de arquivos .xlsx e .xls, tornando este procedimento mais ágil e fácil para o usuário em comparação ao programa original. A interface web modernizou o uso do modelo, permitindo sua utilização em qualquer sistema operacional. A interface em Python facilitará futuras atualizações ao modelo CQESTR.

Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-02T18:48:21Z No. of bitstreams: 1 DiegoDeAzevedoOliveira_DISSERT.pdf: 1039192 bytes, checksum: a387d372d3c8da2d66010f294542538a (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-07-04T13:18:52Z (GMT) No. of bitstreams: 1 DiegoDeAzevedoOliveira_DISSERT.pdf: 1039192 bytes, checksum: a387d372d3c8da2d66010f294542538a (MD5) / Made available in DSpace on 2018-07-04T13:18:53Z (GMT). No. of bitstreams: 1 DiegoDeAzevedoOliveira_DISSERT.pdf: 1039192 bytes, checksum: a387d372d3c8da2d66010f294542538a (MD5) Previous issue date: 2018-02-05 / Softwares precisam ser seguros e corretos. Partindo desse pressuposto, novas tecnologias e técnicas são desenvolvidas para comprovar as competências de um programa. Essa necessidade de segurança se torna mais relevante ao tratar de softwares que atuam em sistemas críticos, como os sistemas ferroviário e aeroviário. A utilização de métodos formais na construção de software busca solucionar o problema. Ao utilizar o método formal B através da plataforma Atelier-B, e após provar os componentes de um projeto é necessária a tradução para a linguagem desejada. Essa tradução ocorre por meio de tradutores e compiladores B. Habitualmente, o processo de compilação em compiladores maduros é seguro, porém não estão completamente livres de falhas e eventualmente erros são encontrados. Ao expandir essa afirmação para tradutores B é necessário cautela, uma vez que esses não são tão comuns e utilizados quanto compiladores que circulam há mais tempo no mercado. Testes de software podem ser utilizados para realizar a análise da tradução. Através de critérios de cobertura é possível inferir o nível de qualidade do software e facilitar a detecção de falhas. Realizar a checagem da cobertura e testes em software pode exigir bastante esforço e tempo, principalmente ao serem realizados manualmente. Para sanar essa demanda, a ferramenta BTestBox visa analisar, de maneira automática, a cobertura atingida por implementações B desenvolvidas através do Atelier-B. BTestBox também testa automaticamente as traduções feitas a partir de implementações B. Para isso, BTestBox utiliza os casos de teste gerados para a verificação de cobertura e compara os valores esperados de saída com os encontrados após a tradução. O processo feito por BTestBox é todo automático e pode ser utilizado a partir do Atelier-B via instalação de plugin com uma interface simples. Essa dissertação apresenta a ferramenta BTestBox. BTestBox foi testado através de pequenas implementações B com os elementos gramaticais possíveis da linguagem B. BTestBox apresenta funcionalidade e vantagens para programadores que utilizam o método formal B. / Software needs to be safe and run smoothly. From that assumption, new technologies and techniques are developed to test the quality of a program. This is more relevant when developing critical systems, such as railways and avionics control systems. Formal methods try to adress this need. When using B in Atelier-B, after proving the components of a project is necessary to translate to the desired language, a translation is made by using B translators and compilers. Usually, the process of compilation is safe when perfomed by mature compilers although they are not free of errors and bugs often crop up. The same reliability is not always observed in B translators since they have been on the market for less time. Software testing may solve and be used to perform the analyses of the translated code. From coverage criteria, it is possible to infer quality of a piece of software and detect bugs. This process is hard and time-consuming, mainly if it is perfomed manually. To address this problem, the BTestBox tool aims to analyze automatically the coverage of B implementations built through Atelier-B. BTestBox also automatically tests the translation from B implementations. For this, BTestBox uses the same test case generated to verify the coverage and compare the output expected values with the values found in the translation. This process is fully automatic and may be started from Atelier-B with a plugin. This thesis presents the tool BTestBox. The tool is a solution to the problems exposed in the previous paragraph. BTestBox was tested with small B implementations and all gramatical elements from B language. It offers various functionalities and advantages to developers that use the B-Method.

Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-30T13:08:13Z No. of bitstreams: 1 CaioFreitasDeOliveira_DISSERT.pdf: 5209631 bytes, checksum: d2308cc568d086c9b77311a9ea1e53fa (MD5) / Approved for entry into archive by clediane guedes (clediane@bczm.ufrn.br) on 2018-07-30T13:12:05Z (GMT) No. of bitstreams: 1 CaioFreitasDeOliveira_DISSERT.pdf: 5209631 bytes, checksum: d2308cc568d086c9b77311a9ea1e53fa (MD5) / Made available in DSpace on 2018-07-30T13:12:05Z (GMT). No. of bitstreams: 1 CaioFreitasDeOliveira_DISSERT.pdf: 5209631 bytes, checksum: d2308cc568d086c9b77311a9ea1e53fa (MD5) Previous issue date: 2016-08-05 / Jogos de estratégia em tempo real (RTS) apresentam muitos desafios para a criação de inteligências artificiais. Um destes desafios é criar um plano de ações efetivo dentro de um dado contexto. Um dos jogos utilizados como plataforma para criação de game AIs competitivas é o StarCraft. Tais game AIs têm dificuldade em se adaptar e criar bons planos para combater a estratégia inimiga. Neste trabalho, um novo modelo de escalonamento de tarefas é proposto modelando os problemas de planejamento em jogos RTS. Este modelo considera eventos cíclicos e consiste em resolver um problema multiobjetivo que satisfaz restrições impostas pelo jogo. São considerados recursos, tarefas e eventos cíclicos que traduzem as características do jogo em um caso do problema. O estado inicial do jogo contém as informações sobre os recursos, tarefas incompletas e eventos ativos. A estratégia define quais recursos maximizar ou minimizar e quais restrições são aplicadas aos recursos, bem como o horizonte de projeto. São investigados quatro otimizadores multiobjetivo: NSGA-II e sua variante focada em joelhos, GRASP e Colônia de Formigas. Experimentos com casos baseados em problemas reais de Starcraft são reportados. / Jogos de estratégia em tempo real (RTS) apresentam muitos desafios para a criação de inteligências artificiais. Um destes desafios é criar um plano de ações efetivo dentro de um dado contexto. Um dos jogos utilizados como plataforma para criação de game AIs competitivas é o StarCraft. Tais game AIs têm dificuldade em se adaptar e criar bons planos para combater a estratégia inimiga. Neste trabalho, um novo modelo de escalonamento de tarefas é proposto modelando os problemas de planejamento em jogos RTS. Este modelo considera eventos cíclicos e consiste em resolver um problema multiobjetivo que satisfaz restrições impostas pelo jogo. São considerados recursos, tarefas e eventos cíclicos que traduzem as características do jogo em um caso do problema. O estado inicial do jogo contém as informações sobre os recursos, tarefas incompletas e eventos ativos. A estratégia define quais recursos maximizar ou minimizar e quais restrições são aplicadas aos recursos, bem como o horizonte de projeto. São investigados quatro otimizadores multiobjetivo: NSGA-II e sua variante focada em joelhos, GRASP e Colônia de Formigas. Experimentos com casos baseados em problemas reais de Starcraft são reportados.

Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-30T13:26:30Z No. of bitstreams: 1 FladsonThiagoOliveiraGomes_DISSERT.pdf: 2012982 bytes, checksum: 32b3a5c5873614b73f362994472d31a9 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-07-30T22:06:38Z (GMT) No. of bitstreams: 1 FladsonThiagoOliveiraGomes_DISSERT.pdf: 2012982 bytes, checksum: 32b3a5c5873614b73f362994472d31a9 (MD5) / Made available in DSpace on 2018-07-30T22:06:38Z (GMT). No. of bitstreams: 1 FladsonThiagoOliveiraGomes_DISSERT.pdf: 2012982 bytes, checksum: 32b3a5c5873614b73f362994472d31a9 (MD5) Previous issue date: 2016-03-03 / Atualmente, a etapa de testes no processo de desenvolvimento de software tornou-se imprescindível para garantir a confiabilidade e qualidade do código em produção. As constantes evoluções na arquitetura e código de um sistema, criam sérios desafios para os desenvolvedores e testadores, uma vez que modificações podem não se comportar como o esperado. Neste contexto surge a necessidade de ferramentas e mecanismos que diminuam o impacto negativo gerado pelas constantes evoluções do sistema. Dentre as ferramentas que analisam esse impacto, poucas apresentam os fluxos de execução entre métodos que foram afetados e nenhuma apresenta como resultado se esses fluxos afetados pela evolução estão ou não cobertos pelos testes. Assim, este trabalho apresenta uma abordagem que tem como objetivo principal: (i) analisar a cobertura de código levando em consideração os fluxos de chamadas existentes no sistema que foram afetados por evoluções de código, assim como os fluxos de execução oriundos da execução dos testes; (ii) indicar quais fluxos de chamadas do sistema que possuem métodos modificados e não estão sendo cobertos pelos testes atualmente e que, portanto, poderiam ser considerados para melhorar a qualidade dos testes; e (iii) indicar se houve degradação na qualidade da suíte de testes. Um estudo empírico foi realizado em 6 sistemas e os resultados mostram que a abordagem conseguiu identificar entre 19% e 92% de fluxos de execução afetados por mudanças que não estão cobertos e ainda que 3 dos 6 sistemas tiveram uma degradação na qualidade dos testes.