???item.export.label??? ???item.export.type.endnote??? ???item.export.type.bibtex???

Please use this identifier to cite or link to this item: https://tede.ufam.edu.br/handle/tede/4091
???metadata.dc.type???: Dissertação
Title: Aplicando verificação de modelos baseada nas teorias do módulo da satisfabilidade para o particionamento de hardware/software em sistemas embarcados
???metadata.dc.creator???: Trindade, Alessandro Bezerra 
???metadata.dc.contributor.advisor1???: Cordeiro, Lucas Carvalho
???metadata.dc.contributor.referee1???: Cordeiro, Lucas Carvalho
???metadata.dc.contributor.referee2???: Costa Filho , Cícero Ferreira Fernandes
???metadata.dc.contributor.referee3???: Pena, Patrícia Nascimento
???metadata.dc.description.resumo???: Quando se realiza um coprojeto de hardware/software para sistemas embarcados, emerge o problema de se decidir qual função do sistema deve ser implementada em hardware (HW) ou em software (SW). Este tipo de problema recebe o nome de particionamento de HW/SW. Na última década, um esforço significante de pesquisa tem sido empregado nesta área. Neste trabalho, são apresentadas duas novas abordagens para resolver o problema de particionamento de HW/SW usando técnicas de verificação formal baseadas nas teorias do módulo da satisfabilidade (SMT). São comparados os resultados obtidos com a tradicional técnica de programação linear inteira (ILP) e com o método moderno de otimização por algoritmo genético (GA). O objetivo é demonstrar, com os resultados empíricos, que as técnicas de verificação de modelos podem ser efetivas, em casos particulares, para encontrar a solução ótima do problema de particionamento de HW/SW usando um verificador de modelos baseado no solucionador SMT, quando comparado com técnicas tradicionais.
Abstract: When performing hardware/software co-design for embedded systems, does emerge the problem of allocating properly which functions of the system should be implemented in hardware (HW) or in software (SW). This problem is known as HW/SW partitioning and in the last ten years, a significant research effort has been carried out in this area. In this proposed project, we present two new approaches to solve the HW/SW partitioning problem by using SMT-based verification techniques, and comparing the results using the traditional technique of Integer Linear Programming (ILP) and a modern method of optimization by Genetic Algorithm (GA). The goal is to show with experimental results that model checking techniques can be effective, in particular cases, to find the optimal solution of the HW/SW partitioning problem using a state-of-the-art model checker based on Satisfiability Modulo Theories (SMT) solvers, when compared to the traditional techniques.
Keywords: Coprojeto hardware/software
Sistemas embarcados
Particionamento
Programação linear inteira
Algoritmo genético
Verificação de modelos
Hardware/software co-design
Embedded systems
Partitioning
Integer linear programming
Genetic algorithm
Model checking
???metadata.dc.subject.cnpq???: ENGENHARIAS: ENGENHARIA ELÉTRICA
Language: por
???metadata.dc.publisher.country???: Brasil
Publisher: Universidade Federal do Amazonas
???metadata.dc.publisher.initials???: UFAM
???metadata.dc.publisher.department???: Faculdade de Tecnologia
???metadata.dc.publisher.program???: Programa de Pós-graduação em Engenharia Elétrica
Citation: TRINDADE, Alessandro Bezerra. Aplicando verificação de modelos baseada nas teorias do módulo da satisfabilidade para o particionamento de hardware/software em sistemas embarcados. 2015. 72 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus, 2015.
???metadata.dc.rights???: Acesso Aberto
URI: http://tede.ufam.edu.br/handle/tede/4091
Issue Date: 9-Feb-2015
Appears in Collections:Mestrado em Engenharia Elétrica

Files in This Item:
File Description SizeFormat 
Dissertação - Alessandro Bezerra Trindade.pdfDissertação - Alessandro Bezerra Trindade.pdf1.79 MBAdobe PDFThumbnail

Download/Open Preview


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.