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
Notícia cadastrada em: 27/01/2012 10:52
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2019 - UFRN - sigaa09-producao.info.ufrn.br.sigaa09-producao