Banca de QUALIFICAÇÃO: IVAN SOARES DE MEDEIROS JUNIOR
Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE: IVAN SOARES DE MEDEIROS JUNIOR
DATA: 20/12/2011
HORA: 14:00
LOCAL: Sala de Reuniões do DIMAp - UFRN
TÍTULO:
Geração Automática de Hardware Verificado
PALAVRAS-CHAVES:
Palavras-chave: Métodos Formais, CSP, Handel-C, ferramentas.
PÁGINAS: 100
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Engenharia de Software
RESUMO:
A remoção de inconsistências em um projeto é menos custosa quando realizadas nas etapas iniciais da sua concepção. A utilização de Métodos Formais melhora a compreensão dos sistemas além de possuir diversas técnicas, como a especificação e verificação formal, para identificar essas inconsistências nas etapas iniciais de um projeto. Porém, a transformação de uma especificação formal para uma linguagem de programação é uma tarefa não trivial, feita manualmente e passível da inserção de erros.
Este trabalho propõe a extensão de uma ferramenta que traduz automaticamente especificações escritas em CSP para Handel-C. CSP é uma linguagem de descrição formal adequada para trabalhar com sistemas concorrentes. Handel-C é uma linguagem de programação cujo resultado pode ser compilado diretamente para FPGA's. A extensão consiste no aumento do conjunto de operadores CSP aceitos pela ferramenta e a adição de um protocolo que elimina algumas restrições da composição paralela de componentes.
Palavras-chave: Métodos Formais, CSP, Handel-C, ferramentas.
A remoção de inconsistências em um projeto é menos custosa quando realizadas nas etapas iniciais da sua concepção. A utilização de Métodos Formais melhora a compreensão dos sistemas além de possuir diversas técnicas, como a especificação e verificação formal, para identificar essas inconsistências nas etapas iniciais de um projeto. Porém, a transformação de uma especificação formal para uma linguagem de programação é uma tarefa não trivial, feita manualmente e passível da inserção de erros.
Este trabalho propõe a extensão de uma ferramenta que traduz automaticamente especificações escritas em CSP para Handel-C. CSP é uma linguagem de descrição formal adequada para trabalhar com sistemas concorrentes. Handel-C é uma linguagem de programação cujo resultado pode ser compilado diretamente para FPGA's. A extensão consiste no aumento do conjunto de operadores CSP aceitos pela ferramenta e a adição de um protocolo que elimina algumas restrições da composição paralela de componentes.
MEMBROS DA BANCA:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1694485 - MARCIO EDUARDO KREUTZ
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE