Aplicando verificação de modelos baseada nas teorias do módulo da satisfabilidade para o particionamento de hardware/software em sistemas embarcados

• Ano de defesa: 2015
• Autor(a) principal: Trindade, Alessandro Bezerra
• Outros Autores: http://lattes.cnpq.br/4511445991061477
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal do Amazonas; Faculdade de Tecnologia; Brasil; UFAM; Programa de Pós-graduação em Engenharia Elétrica
• Palavras-chave em Português: 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; ENGENHARIAS: ENGENHARIA ELÉTRICA
• Link de acesso: http://tede.ufam.edu.br/handle/tede/4091

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.