Tipo de documento:	Relatório de Pesquisa
Título:	Verificação de Modelos de Hardware que Usam a Biblioteca do SystemC
Autor(a):	Luciano Nunes Sobral
Orientador(a):	Lucas Carvalho Cordeiro
Resumo:	Projetar softwares embarcados tem sido uma tarefa que exige uma execução próxima à perfeição, uma vez que a nossa dependência ao funcionamento correto desses sistemas tem aumentado rapidamente, de forma que um erro, falha ou bug pode causar prejuízos altíssimos à sociedade. Os sistemas embarcados são utilizados em um enorme leque de aplicações, tais como: Sistema de controle de air-bag, setup-boxes, telefones celulares e até aparelhos complexos utilizados na medicina. Estes sistemas estão se tornando cada vez mais complexos e requerem processadores multi-core com memória compartilhada escalável para atender a crescente demanda do poder computacional. Desta maneira, a confiabilidade dos sistemas (distribuídos) embarcados é um assunto chave no desenvolvimento de sistemas. As empresas procuram formas mais rápidas e baratas para verificar a confiabilidade dos seus sistemas, evitando assim grandes prejuízos. Uma das formas mais eficazes e de mais baixo custo é a verificação de modelos (ou model checking). Apesar da eficácia desse método de verificação, existem muitos sistemas que não podem ser verificados de forma automática pelo fato de não existir (ou existir parcialmente) no mercado um verificador que englobe determinadas linguagens, bibliotecas e frameworks. Um bom exemplo disso, são os sistemas de hardware que utilizam o SystemC ( biblioteca de classes e macros para C++ ). Neste projeto de pesquisa, nós investigaremos, a partir de análise de circuitos de hardware reais, quais são as funcionalidades mais utilizadas da biblioteca SystemC no mercado, definindo assim uma estrutura de como será feita a verificação de circuitos digitais que utilizam essa biblioteca. É importante salientar que o acadêmico irá ter contato com o estado da arte da sub-área de Verificação Formal de Hardware/Software. Além disso, o acadêmico terá contato com a implementação e uso de algoritmos de complexidade exponencial, analisará aplicações reais, e desenvolverá habilidades de desenvolvimento com a linguagem de programação C++.
Palavras-chave:	Métodos Formais Verificação de Hardware SystemC
Área de conhecimento - CNPQ:	ENGENHARIAS
Idioma:	pt_BR
País de publicação:	Brasil
Editor:	Universidade Federal do Amazonas
Sigla da Instituição:	UFAM
Faculdade, Instituto ou Departamento:	Faculdade de Tecnologia Faculdade de Tecnologia
Nome do programa:	PROGRAMA PIBIC 2012
Tipo de acesso:	Acesso Aberto
URI:	http://riu.ufam.edu.br/handle/prefix/3213
Data do documento:	31-jul-2013
Aparece nas coleções:	Relatórios finais de Iniciação Científica - Engenharias

Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.