Personality of software engineering professionals has been a continuous element of interest in academic research. Researchers have applied different models of personality analysis in various software engineering areas to identify improvement points, to promote job satisfaction and to better organize teams. Among these models, we can highlight the MBTI and BIG Five. This work aims to conduct a study to evaluate personality models applied in software engineering and to understand how human personality influences software quality. Two controlled experiments were performed, the first in industry, in IT department of a private higher education institution and the second in an advanced programming discipline in academy. For both experiments, the quality of software individually produced by each participant was evaluated using software metrics for object-oriented paradigm languages. As a result, there is evidence that developers with different personalities do not develop software of equal quality. As the experiments were run in a single geographic location with an own software development culture, additional studies need to be performed to determine any real link between personality and software quality. / A personalidade dos profissionais de engenharia de software tem sido um elemento contínuo de interesse na pesquisa acadêmica. Os pesquisadores aplicaram diferentes modelos de análise de personalidade em várias áreas de engenharia de software para identificar pontos de melhoria, promover a satisfação no trabalho e organizar melhor as equipes. Entre esses modelos destacamos o MBTI e BIG Five. Esta dissertação objetiva realizar um estudo para avaliar modelos de personalidade aplicados em engenharia de software e compreender como a personalidade humana influencia a qualidade do software. Dois experimentos controlados foram realizados, o primeiro na indústria, no departamento de TI de uma instituição privada de ensino superior e o segundo em uma disciplina de programação avançada na academia. Para ambas as experiências, a qualidade do software produzido individualmente por cada participante foi avaliada utilizando métricas de software para linguagens de paradigma orientadas a objetos. Como resultado, há evidências de que desenvolvedores com personalidades diferentes não desenvolvem software de qualidade igual. Como os experimentos foram realizados em uma única localização geográfica com uma cultura de desenvolvimento de software própria, estudos adicionais precisam ser realizados para determinar qualquer ligação real entre personalidade e qualidade de software.

This work has the goal to make an implementation of an anonymization service on Software-Defined Networks (SDN) with the goal to reduce the number of attacks. With an anonymization service is possible to hide the IP address from the network’s hosts, ensuring more protection against security attacks, which allows a more time availability. One of the biggest challenge on SDN architecture is the security issue. The separation of control and data planes allows o generated challenges on security, due to the network’s permissiveness to attacks such as “ Man in the Middle ”, Denial of Service and Saturation. The service developed in this work, named as BomIP, uses the micro-data anonymization technique of randomization of IP address of the hosts. The BomIP was added in the SDN controller RunOS, which was the responsible to make the management of the real and anonymized IP address. To validate this service it was developed two Case Studies with an environment simulating a Denial of Service attack. The first Case Study made a comparison between Crypto-Pan and BomIP. While the second Case Study made a comparison between a traditional network IP and a SDN one using BomIP, both under Denial of Service attack. The analysis of results showed that the service developed has an running time 65% more efficient than Crypto-Pan. The assintotic analysis shows that BomIP is an algorith with running time of quadratic order. The results also showed that the anonymized packets can be tracked and a mitigation of 80% from the attacks trials, ensuring that the services provided by the network remain available. / Este trabalho tem como objetivo implementar um servi¸co de anonimiza¸c˜ao em Redes Definidas por Software (SDN) com o objetivo de realizar a mitiga¸c˜ao de tentativas de ataque sofridas por uma rede. Atrav´es de um servi¸co de anonimiza¸c˜ao ´e poss´ıvel realizar a oculta¸c˜ao dos endere¸cos IP dos hosts da rede, garantindo maior prote¸c˜ao contra ataques `a seguran¸ca, permitindo um aumento de sua disponibilidade. Um dos maiores desafios da arquitetura SDN ´e a seguran¸ca. A separa¸c˜ao do controle e do plano de dados permite que desafios para garantir a seguran¸ca sejam gerados, devido `a permissividade da rede a ataques como “Homem no Meio”, Nega¸c˜ao de Servi¸co e Satura¸c˜ao. O servi¸co aqui desenvolvido, denominado de BomIP, utiliza a t´ecnica de anonimiza¸c˜ao de micro-dados atrav´es da randomiza¸c˜ao dos endere¸cos IP dos hosts. O servi¸co BomIP foi adicionado ao controlador RunOS, que ficou respons´avel por realizar o gerenciamento dos endere¸cos IP reais e anonimizados. Para validar este servi¸co foram realizados dois Estudos de Caso em um ambiente simulando um ataque de Nega¸c˜ao de Servi¸co. O primeiro Estudo de Caso realizou a compara¸c˜ao do funcionamento do servi¸co de anonimiza¸c˜ao Crypto-Pan com o BomIP. Enquanto que o segundo Estudo de Caso realizou a compara¸c˜ao de uma rede IP tradicional sob ataque de Nega¸c˜ao de Servi¸co e uma SDN utilizando o BomIP. A an´alise dos resultados mostrou que o servi¸co desenvolvido tem um tempo de execu¸c˜ao 65% mais eficiente que o Crypto-Pan. A an´alise de complexidade do algoritmo do BomIP demonstrou que ´e de ordem quadr´atica. Os resultados tamb´em demonstraram que os pacotes anonimizados permitem a rastreabilidade e a mitiga¸c˜ao de 80% das tentativas de ataque, dando garantias que os servi¸cos providos pela rede continuem dispon´ıveis.

Made available in DSpace on 2015-04-11T14:03:11Z (GMT). No. of bitstreams: 1 Dissertacao Leonardo Nascimento dos Santos.pdf: 3849234 bytes, checksum: 578fe47a5b307904388da382d7f5484b (MD5) Previous issue date: 2009-03-31 / Fundação de Amparo à Pesquisa do Estado do Amazonas / Work and learning built individually and in groups took a new and definitive impulse from popularization of software tools that currently compose web-based virtual environments. After a time of reckoning and appropriation of these resources, work, teaching, learning and social relations started to demand that virtual environments cannot yet answer, partially due to need of conformation by some of these environments to certain functional aspects maintained mainly by tradition. A possible strategy to deal with this problem is to devise and to develop flexible environments to support cooperative activities, given users a better balance between supporting tools and goals and profiles of participants in a specific activity. This work is part of a multi-institutional effort on the area where, from conceptual elements defining an innovative and simple approach to development of virtual environments, it is reported the organization, modeling and implementation of an instance of this kind of environment. The resulting prototype, currently in use at UFAM, was built using Moodle as development and evaluation platform. / O trabalho e a aprendizagem construídos individual e coletivamente tomaram novo e determinante impulso a partir da disseminação das ferramentas de software que atualmente compõem os ambientes virtuais baseados na Web. Após um período de reconhecimento e apropriação desses recursos, o trabalho, o ensino, a aprendizagem e as relações sociais como um todo passam a apresentar demandas que os ambientes virtuais ainda não conseguem atender, em parte devido à conformação desses ambientes a certos aspectos funcionais mantidos principalmente por tradição. Uma estratégia possível para tratar esse problema é a concepção e desenvolvimento de ambientes flexíveis para apoiar a realização de atividades cooperativas, propiciando aos usuários uma melhor sintonia entre ferramentas de apoio e os objetivos e os perfis dos participantes de uma determinada atividade. O trabalho aqui descrito faz parte de um esforço multi-institucional de pesquisa no tema, onde, a partir dos elementos conceituais que definem uma abordagem de inovadora simplicidade à concepção e desenvolvimento de ambientes virtuais, é relatada a organização, modelagem e implementação de uma instância desse tipo de ambiente. O protótipo resultante, atualmente em plena utilização na UFAM, foi construído utilizando o Moodle como plataforma de desenvolvimento e avaliação.

Este trabalho aborda a utilização do método de Lattice Boltzmann como ferramenta de simulação para a área de dinâmica de fluidos. Além disso, apresenta o programa LBSim desenvolvido durante o período de pesquisa, construído para ser flexível e extensível (através do emprego de técnicas de orientação a objetos) e com uma interface gráfica mais amigável do que outros projetos semelhantes. Como resultado deste trabalho, o software LBSim implementa uma série de módulos diferentes que utilizam o método de Lattice Boltzmann como base, permitindo a simulação de casos monofásico, multifásico, multicomponente, com suporte à gravidade, meios porosos, difusão, transferência de calor e paredes deslizantes. / This work approaches the use of the Lattice Boltzmann method as a simulation tool for the fluid dynamics area. Beyond that, it presents the LBSim software, developed during the period of the research and built to be flexible and extensible (through the application of techniques of the object oriented paradigm) and with a graphical interface more friendly than other similar projects. As a result of this work, the LBSim software implements a series of different modules that uses the Lattice Boltzmann method as a base, allowing the simulations of the following cases: monophase, multiphase, multicomponent, with support of gravity, porous media, diffusion, heat transfer and moving walls.

O uso de análise quantitativa em radiologia médica tem sido de grande valia na detecção de alterações não acessíveis à análise visual simples, dita qualitativa, seja por serem muito sutis, seja por não estarem presentes nas técnicas de imagem de ressonância magnética convencional. Porém, certos tipos de quantificação exigem a aquisição softwares e de plataformas computacionais de alto custo, além de mão de obra especializada com conhecimento técnico em computação para operar em ambientes não intuitivos. Neste cenário o objetivo deste trabalho foi a implementação de um software para análise de transferência de magnetização em imagens de ressonância magnética nuclear que funcionasse na plataforma IBM-PC e em sistemas operacionais livres como GNU/Linux. Com este intuito foi elaborado um algoritmo para leitura de imagens codificadas no padrão DICOM 3.0, um algoritmo para a construção dos mapas de Razão de Transferência de Magnetização do volume adquirido e um visualizador com interface amigável para a segmentação e análise dos resultados. Ao final, software possibilitou a abertura da imagem DICOM. Também construiu de maneira eficiente, os mapas de diferença de porcentagem entre as imagens sem e com o pulso de transferência de magnetização (MTR), possibilitando, inclusive, correções de artefatos de movimentos, quando pouco intensos. Permitiu o delineamento de regiões de interesse irregular, com boa visibilidade dos resultados. Como controle padrão, os resultados foram comparados com o conjunto de ferramentas da Universidade McGill (Brain Imaging Center, McGuill University, Montreal, Quebec, Canadá), amplamente testado em artigos publicados. / The use of quantitative analysis in medical radiology has been of great value in the detection of not accessible alterations in the simple visual analysis, said qualitative, for being very subtle, or for not being present in conventional magnetic resonance image techniques. However, certain types of quantification demand the acquisition of high cost softwares and computational platforms, beyond specialized workmanship, with technical knowledge in computation, to operate in non intuitive environments. In this scenery the objective of this work was the implementation of a software for analysis of transference of magneti zation in nuclear magnetic resonance images that works in IBM-PC platform and free operational systems as GNU/Linux. So, an algorithm for reading of standard DICOM 3.0 codified images was elaborated, an algorithm for the construction of Magnetization Transfer Ratio maps of acquired volume, and a visualizer with friendly interface for segmentation and analysis of the results. Finally the software made the opening of DICOM image possible. It also generated in efficient way the maps of percentage difference among the images without and with the pulse of magnetization transfer (MT), also making devices of movement corrections possible, when they are not very intense. It allowed the delineation of regions of irregular interest, with good visibility of the results. As standard control, the results were compared with the set of tools of the McGill University (Brain Imaging Center, McGuill University, Montreal, Quebec, Canada), widely tested in published articles. The elaborated program took care of the considered objectives.

Os Sistemas Distribuídos (SDs) tem apresentado uma crescente complexidade no seu gerenciamento, além de possuir a necessidade de garantir Qualidade de Serviço (QoS) aos seus usuários. A Computação Autonômica (CA) surge como uma forma de transformar os SDs em Sistemas Distribuídos Autonômicos (SDAs), com capacidade de auto-gerenciamento. Entretanto, não foi encontrado um processo de desenvolvimento de software, focado na criação de SDAs. Na grande maioria dos trabalhos relacionados, simplesmente é apresentado um SD, juntamente com qual aspecto da CA deseja-se implementar, a técnica usada e os resultados obtidos. Isso é apenas uma parte do desenvolvimento de um SDA, não abordando desde a definição dos requisitos até a manutenção do software. Mais importante, não mostra como tais requisitos podem ser formalizados e posteriormente solucionados por meio do auto-gerenciamento fornecido pela CA. Esta tese foca na proposta de um processo de desenvolvimento de software voltado para SDAs. Com esse objetivo, foram integradas diferentes áreas de conhecimento, compreendendo: Processo Unificado de Desenvolvimento de Software (PU), SDs, CA, Pesquisa Operacional (PO) e Avaliação de Desempenho de Sistemas Computacionais (ADSC). A prova de conceito foi feita por meio de três estudos de caso, todos focando-se em problemas NP-Difícil, são eles: (i) otimização off-line (problema da mochila com múltiplas escolhas), (ii) otimização online (problema da mochila com múltiplas escolhas) e (iii) criação do módulo planejador de um gerenciador autonômico, visando realizar o escalonamento de requisições (problema de atribuição generalizado). Os resultados do primeiro estudo de caso, mostram que é possível usar PO e ADSC para definir uma arquitetura de base para o SDA em questão, bem como reduzir o tamanho do espaço de busca quando o SDA estiver em execução. O segundo, prova que é possível garantir a QoS do SDA durante sua execução, usando a formalização fornecida pela PO e sua respectiva solução. O terceiro, prova que é possível usar a PO para formalizar o problema de auto-gerenciamento, bem como a ADSC para avaliar diferentes algoritmos ou modelos de arquitetura para o SDA. / Distributed Systems (DSs) have an increasing complexity and do not have their management, besides having a quality of service (QoS) to its users. Autonomic Computing (AC) emerges as a way of transforming the SDs into Autonomous Distributed Systems (ADSs), with a capacity for self-management. However, your software development process is focused on creating SDAs. In the vast majority of related works, simply an SD model, along with what aspect of the AC implement, a technique used and the results obtained. This is only a part of the development of an ADS, not approaching from an definition of requirements for a maintenance of software. More importantly, it does not show how such requirements can be formalized and subsequently solved through the self-management provided by AC. This proposal aims at a software development process for the DASs. To this end, different areas of knowledge were integrated, including: Unified Software Development Process (PU), SDs, CA, Operations Research (OR) and Computer Systems Performance Evaluation (CSPE). The proof of concept was made through three case studies, all focusing on NP-Hard problems, namely: (i) off-line optimization (problem of the backpack with multiple choices), (ii) (Problem of the backpack with multiple choices) and (iii) creation of the scheduling module of an autonomic manager, aiming to carry out the scheduling of requests (problem of generalized assignment). The results of the first case study show that it is possible to use OR and CSPE to define a base architecture for the DAS in question, as well as reduce the size of the search space when SDA is running. The second, proves that it is possible to guarantee the QoS of the DAS during its execution, using the formalization provided by the OR and its respective solution. The third, proves that it is possible to use the PO to formalize the self-management problem, as well as the ADSC to evaluate different algorithms or architecture models for the ADS.

Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário. / Formal specifications are useful for describing what a system should do, without defining how, and, owing to its formal nature, it is possible to analyse them systematically. However useful formal specifications are, their usage as part of the software development process is rather rare. This is, in part, due to the scarcity of both methodologies and tools that support this development. The first goal of this work is to define a software development methodology that enables the developer to produce a Java application from a formal specification written in Z. This methodology will rely strongly on the generation of Java application skeletons and instrumentation of the generated code with means of verifying conditions (invariants, pre and post-conditions) e tracing violations of these conditions. Through this mechanisms, it is possible to mix formal and informal development in the global software development process. The second goal of this work is to develop a tool that will implement part of this methodology, producing a partial implementation that must be complemented by the developer.

Submitted by Nadir Basilio (nadirsb@uninove.br) on 2016-07-01T14:26:09Z No. of bitstreams: 1 Paulo Henrique Ribeiro De Oliveira.pdf: 2464979 bytes, checksum: 93b7213ac2b763d9ce75892da0e93cda (MD5) / Made available in DSpace on 2016-07-01T14:26:09Z (GMT). No. of bitstreams: 1 Paulo Henrique Ribeiro De Oliveira.pdf: 2464979 bytes, checksum: 93b7213ac2b763d9ce75892da0e93cda (MD5) Previous issue date: 2016-02-29 / The effort spent in maintaining systems regarded as legacies is relatively higher than that of new projects development effort. Such systems should be kept in place because, in most cases, are difficult to replace, given the complexity of changing the interaction and the impact on the functioning of processes, ie, the system can not stop. Thus, maintenance or modifications represent a sign of success for a Legacy System because it means that it is still useful and worth investing resources to keep it updated and running. However, if changes are carried out due to an emergency on business dynamics, and proper documentation is not completed, problems involving control and management of future maintenance might arise. In this context, it is the Requirements Engineering´s responsibility, as a sub-area of Software Engineering, to improve processes by proposing methods, tools and techniques that promote the development of the Requirement´s documentation, so that the requirements are in accordance with the satisfaction of stakeholders, meeting the business attributes in question. The objective of this work was to apply the Requirements Engineering in Legacy Systems of Management and Costing Methods of Sales Proposals in the stamping industry. Through literature review, document analysis and action research, the study was divided into four phases considering the development of the Sales Proposal Management and Costing Method System and three maintenance stages performed with the application of Requirements Engineering. In the first phase, a group of artifacts was generated expressing all system features. In the second phase, a progressive maintenance incorporated new features based in the system´s backlog with requirements collected in the first phase. The third phase included a new stamping business area that was not present in the initial development. Lastly, the fourth phase included new maintenance adjustments that answered to the needs of the stamping business system. The results of the study phases proved that the processes described in the Requirements Engineering (RE) were present in the information gathering actions, analysis, documentation and verification and validation of requirements, bringing academic and technical knowledge on issues related to legacy systems, ER and Software Engineering. As a result, it was concluded that the Requirements Engineering can be applied to Legacy Systems of Management and Costing Methods of Sales Proposals in stamping company in the industry. / O esforço despendido para a manutenção de sistemas considerados como legado é relativamente maior que o esforço de desenvolvimento de novos projetos. Tais sistemas devem ser mantidos em funcionamento pois, em sua maioria, são de difícil substituição, dada a complexidade de convívio da mudança e o impacto no funcionamento dos processos, ou seja, o sistema não pode parar. Dessa forma, manutenções ou modificações representam um sinal de sucesso para um sistema legado, pois significam que ele ainda é útil e que vale a pena investir recursos para mantê-lo atualizado e em funcionamento. No entanto, se modificações são realizadas emergencialmente devido a dinâmica do negócio, e a devida documentação não é realizada, tem-se instaurado o caos para o controle e gerência de futuras manutenções. Neste contexto, cabe à Engenharia de Requisitos, como sub-área da Engenharia de Software, aperfeiçoar os processos para o gerenciamento do ciclo de vida dos requisitos propondo métodos, ferramentas e técnicas que promovam o desenvolvimento do documento de requisitos, para que os requisitos estejam em conformidade com a satisfação dos stakeholders, atendendo as características do negócio em questão. Assim, o objetivo deste trabalho foi aplicar a Engenharia de Requisitos em Sistema Legado de Gestão e Custeio de Propostas Comerciais em empresa do setor de estamparia. Por meio de levantamento bibliográfico, análise documental e pesquisa-ação, o estudo foi dividido em quatro fases considerando o desenvolvimento do Sistema de Gestão e Custeio de Propostas Comerciais e três manutenções realizadas com a aplicação da Engenharia de Requisitos. Na primeira fase um conjunto de artefatos foi gerado expressando todas as funcionalidades do sistema. Na segunda fase uma manutenção evolutiva incorporou novas funcionalidades no sistema baseada em requisitos de backlog coletados na primeira fase. A terceira fase incluiu uma nova área de negócios da estamparia que não esteve presente no desenvolvimento inicial e a quarta fase contemplou novas manutenções ajustando o sistema as necessidades de negócio da estamparia. Os resultados das fases do estudo possibilitaram identificar que os processos descritos na Engenharia de Requisitos (ER) se fizeram presentes nas ações de levantamento, análise, documentação e verificação e validação de requisitos trazendo conhecimento acadêmico e técnico nos temas relacionados a sistemas legados, ER e Engenharia de Software. Concluiu-se, então, que a Engenharia de Requisitos pode ser aplicada em Sistema Legado de Gestão e Custeio de Propostas Comerciais em empresa do setor de estamparia.

Submitted by Nadir Basilio (nadirsb@uninove.br) on 2017-06-06T20:11:59Z No. of bitstreams: 1 Roberto de Souza Goes.pdf: 1689251 bytes, checksum: 72e570131062ac24f1964e0d4ff56a3b (MD5) / Made available in DSpace on 2017-06-06T20:11:59Z (GMT). No. of bitstreams: 1 Roberto de Souza Goes.pdf: 1689251 bytes, checksum: 72e570131062ac24f1964e0d4ff56a3b (MD5) Previous issue date: 2017-04-28 / Design Thinking and agile methods, when used in an innovative and dynamic environment, aiming the creating products and solutions to support business and to increase satisfaction, bringing solutions to the current problems and that also generate future business for the company. This study was carried out with the objective of verifying how the companies that adopted the Design Thinking and the agile methods did to integrate it, from the creation of the solution of the initiatives to be development-using software. Design Thinking is able to aid in the generation of new ideas centered on the human, through research and prototyping techniques, in a fast and multidisciplinary way. Agile methods are widely used and studied as a method of software development. This study was carried out through a multiple case study with data collection for a qualitative research, in companies or in technology departments, where this technology is used as the main tool to manage and generate business. On this research was found three different types of integration between the models, sequentially. The first with a queue between the final solution definition stage and the beginning of software development, the second, without a queue between the final solution definition stage and the beginning of software development, the third model is the use of Design Thinking and agile methods together and simultaneously, as a single process. These different integration models aim to meet the projects needs regarding to complexity and size, as well as the uncertainties in which companies are subject throughout project life cycle. / O Design Thinking e os métodos ágeis, são utilizados em um ambiente inovador e dinâmico, com o objetivo de criar produtos e soluções que gerem maior satisfação para o negócio, de modo que traga soluções para os problemas atuais e que também gerem futuros negócios para a empresa. Este estudo foi realizado com o objetivo de verificar como as empresas que adotaram o Design Thinking e os métodos ágeis fizeram para integrá-los, desde a criação da solução das iniciativas até o seu desenvolvimento através de software. O Design Thinking é capaz de auxiliar na geração novas ideias centradas no humano, por meio de técnicas de pesquisa e prototipação, de maneira rápida e multidisciplinar. Os métodos ágeis são utilizados de maneira amplamente divulgada e estudada como método de desenvolvimento de software. Esta pesquisa foi realizada por meio de estudo de caso múltiplo do tipo incorporado, com coleta de dados por meio de pesquisa qualitativa, em empresas ou departamentos na área de tecnologia, nas quais essa tecnologia é utilizada como principal ferramenta para gerir e gerar negócios. No estudo foram encontrados três tipos diferentes de integração entre os modelos, de modo sequencial, sendo que o primeiro possuía fila entre a etapa final de definição da solução e o início do desenvolvimento do software; o segundo não possui essa característica, o terceiro modelo era a aplicação do Design Thinking e dos métodos ágeis de modo conjunto e simultâneo, isso como um único processo. Estes modos diferentes de integração visavam atender as características dos projetos com relação à complexidade e porte, além das incertezas em que as empresas estiveram sujeitas durante o curso do projeto.

Nesta tese apresentamos o projeto e a implementação do KEMS, um provador de teoremas multi-estratégia baseado no método de tablôs KE. Um provador de teoremas multi-estratégia é um provador de teoremas onde podemos variar as estratégias utilizadas sem modificar o núcleo da implementação. Além de multi-estratégia, o KEMS é capaz de provar teoremas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi. Listamos abaixo algumas das contribuições deste trabalho: * um sistema KE para mbC que é analítico, correto e completo; * um sistema KE para mCi que é correto e completo; * um provador de teoremas multi-estratégia com as seguintes características: - aceita problemas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi; - tem seis estratégias implementadas para lógica clássica proposicional, duas para mbC e duas para mCi; - tem treze ordenadores que são usados em conjunto com as estratégias; - implementa regras simplificadoras para lógica clássica proposicional; - possui uma interface gráfica que permite a visualização de provas; - é de código aberto e está disponível na Internet em http://kems.iv.fapesp.br; * benchmarks obtidos através da comparação das estratégias para lógica clássica proposicional resolvendo várias famílias de problemas; - sete famílias de problemas para avaliar provadores de teoremas paraconsistentes; * os primeiros benchmarks para as famílias de problemas para avaliar provadores de teoremas paraconsistentes. / In this thesis we present the design and implementation of KEMS, a multi-strategy theorem prover based on the KE tableau inference system. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. Besides being multi-strategy, KEMS is capable of proving theorems in three logical systems: classical propositional logic, mbC and mCi. We list below some of the contributions of this work: * an analytic, correct and complete KE system for mbC; * a correct and complete KE system for mCi; * a multi-strategy prover with the following characteristics: - accepts problems in three logical systems: classical propositional logic, mbC and mCi; - has 6 implemented strategies for classical propositional logic, 2 for mbC and 2 for mCi; - has 13 sorters to be used alongside with the strategies; - implements simplification rules of classical propositional logic; - provides a proof viewer with a graphical user interface; - it is open source and available on the internet at http://kems.iv.fapesp.br; * benchmark results obtained by KEMS comparing its classical propositional logic strategies with several problem families; * seven problem families designed to evaluate provers for logics of formal inconsistency; * the first benchmark results for the problem families designed to evaluate provers for logics of formal inconsistency.