Dissertação

{en_GB=SoC-FPGA Accelerated BDD-Based Model Checking} {} EVALUATED

{pt=Verificação de Modelos é considerada uma das ferramentas mais importantes em verificação formal, geralmente usada para verificar requerimentos de hardware e software. Uma das mais importantes descobertas em verificação de modelos foi o uso de Diagramas de Decisão Binária (Binary Decision Diagrams) para melhorar significativamente o tempo de execução e permitir abordar problemas maiores. Devido ao problema fundamental associado a sistemas que exploram espaços de estados, Verificadores de Modelos são considerados demasiado dispendiosos em relação ao tempo gasto para serem amplamente utilizados. Neste trabalho, propomos uma arquitetura HW/SW que usa um dispositivo SoC-FPGA para melhorar o tempo de execução de Verificador de Modelos baseados em BDD. Desenvolvemos uma arquitetura base e duas modificações para um total de quatro arquiteturas diferentes. O resultado final chega perto, mas não melhora as implementações de software em termos de performance relativa., en=Model Checking is considered one of the most important tools in formal verification, commonly used to verify hardware and software requirements. One of most important breakthroughs in Model Checking was the use of \gls{BDDs} to significantly improve the run time and allowing to tackle larger problems. Because of the fundamental problem that plagues state space exploration systems, Model Checkers are considered too much time consuming in order to be widely used. In this paper, we propose a HW/SW architecture that uses SoC-FPGA devices to improve BDD based Model Checkers runtimes. We develop a base architecture and two modifications for a total of four different architectures. The end result comes close but does not improve in terms of performance with regards to a full software implementation.}
{pt=Verificação de Modelos, Diagramas de Decisão Binária, SoC-FPGA, Sistema Hardware/Software, en=Model Checking, Binary Decision Diagram, SoC-FPGA, Hardware/Software System}

janeiro 26, 2021, 16:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Rui António Policarpo Duarte

INESC-ID

Investigador

ORIENTADOR

Pedro Tiago Gonçalves Monteiro

Departamento de Engenharia Informática (DEI)

Professor Auxiliar