Geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução /

Mostrar outras versões (1)

Resumo: A remoção de inconsistências em um projeto é menos custosa quando realizada 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ê...

ver descrição completa

Na minha lista:

Detalhes bibliográficos
Principais autores:	Medeiros Júnior, Ivan Soares de., Oliveira, Marcel Vinicius Medeiros., Universidade Federal do Rio Grande do Norte.
Formato:	Dissertação
Publicado em:
Assuntos:	Engenharia de software - Dissertação. Métodos formais - Linguagem de descrição formal CSPm - Linguagem de programação Handel-C - Geração de código - Formal description language CSPM. Programming language Handel-C.
Endereço do item:	https://repositorio.ufrn.br/jspui/bitstream/123456789/18052/1/IvanSMJ_DISSERT.pdf
Tags:	Adicionar Tag Sem tags, seja o primeiro a adicionar uma tag!

id	oai:localhost:123456789-124011
record_format	dspace
spelling	oai:localhost:123456789-1240112022-11-30T23:06:54Z Geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução / Medeiros Júnior, Ivan Soares de. Oliveira, Marcel Vinicius Medeiros. Universidade Federal do Rio Grande do Norte. Engenharia de software - Dissertação. Métodos formais - Dissertação. Linguagem de descrição formal CSPm - Dissertação. Linguagem de programação Handel-C - Dissertação. Geração de código - Dissertação. Formal description language CSPM. Programming language Handel-C. Resumo: A remoção de inconsistências em um projeto é menos custosa quando realizada 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. Quando feita manualmente, é uma tarefa passível da inserção de erros. O uso de ferramentas que auxiliem esta etapa pode proporcionar grandes benefícios ao produto final que será desenvolvido. Este trabalho propõe a extensão de uma ferramenta cujo foco é a tradução automática de especificações em CSPM para Handel-C. CSP é uma linguagem de descrição formal adequada para trabalhar com sistemas concorrentes, CSPM é a notação utilizada pelas ferramentas de apoio da linguagem. Handel-C é uma linguagem de programação cujo resultado pode ser compilado diretamente para FPGA s. A extensão consiste no aumento no número de operadores CSPM aceitos pela ferramenta, permitindo ao usuário definir processos locais, renomear canais e utilizar guarda booleana em escolhas externas. Além disto, propomos também a implementação de um protocolo de comunicação que elimina algumas restrições da composição paralela de processos na tradução para Handel-C, permitindo que a comunicação em um mesmo canal entre múltiplos processos possa ser mapeada de maneira consistente e que no código gerado não ocorra comunicações indevidas em um canal, ou seja, comunicações que não são permitidas na especificação do sistema.#$&Abstract: Removing inconsistencies in a project is a less expensive activity when done in the early steps of design. The use of formal methods improves the understanding of systems. They have various techniques such as formal specification and verification to identify these problems in the initial stages of a project. However, the transformation from a formal specification into a programming language is a non-trivial task and error prone, specially when done manually. The aid of tools at this stage can bring great benefits to the final product to be developed. This paper proposes the extension of a tool whose focus is the automatic translation of specifications written in CSPM into Handel-C. CSP is a formal description language suitable for concurrent systems, and CSPM is the notation used in tools support. Handel-C is a programming language whose result can be compiled directly into FPGA s. Our extension increases the number of CSPM operators accepted by the tool, allowing the user to define local processes, to rename channels in a process and to use Boolean guards on external choices. In addition, we also propose the implementation of a communication protocol that eliminates some restrictions on parallel composition of processes in the translation into Handel-C, allowing communication in a same channel between multiple processes to be mapped in a consistent manner and that improper communication in a channel does not ocurr in the generated code, ie, communications that are not allowed in the system specification. 1 2022-10-06T06:08:25Z 2022-10-06T06:08:25Z 2012. Dissertação 004.41 M488g DISSERT 188865 https://repositorio.ufrn.br/jspui/bitstream/123456789/18052/1/IvanSMJ_DISSERT.pdf https://repositorio.ufrn.br/jspui/bitstream/123456789/18052/1/IvanSMJ_DISSERT.pdf
institution	Acervo SISBI
collection	SIGAA
topic	Engenharia de software - Dissertação. Métodos formais - Dissertação. Linguagem de descrição formal CSPm - Dissertação. Linguagem de programação Handel-C - Dissertação. Geração de código - Dissertação. Formal description language CSPM. Programming language Handel-C.
spellingShingle	Engenharia de software - Dissertação. Métodos formais - Dissertação. Linguagem de descrição formal CSPm - Dissertação. Linguagem de programação Handel-C - Dissertação. Geração de código - Dissertação. Formal description language CSPM. Programming language Handel-C. Medeiros Júnior, Ivan Soares de. Oliveira, Marcel Vinicius Medeiros. Universidade Federal do Rio Grande do Norte. Geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução /
description	Resumo: A remoção de inconsistências em um projeto é menos custosa quando realizada 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. Quando feita manualmente, é uma tarefa passível da inserção de erros. O uso de ferramentas que auxiliem esta etapa pode proporcionar grandes benefícios ao produto final que será desenvolvido. Este trabalho propõe a extensão de uma ferramenta cujo foco é a tradução automática de especificações em CSPM para Handel-C. CSP é uma linguagem de descrição formal adequada para trabalhar com sistemas concorrentes, CSPM é a notação utilizada pelas ferramentas de apoio da linguagem. Handel-C é uma linguagem de programação cujo resultado pode ser compilado diretamente para FPGA s. A extensão consiste no aumento no número de operadores CSPM aceitos pela ferramenta, permitindo ao usuário definir processos locais, renomear canais e utilizar guarda booleana em escolhas externas. Além disto, propomos também a implementação de um protocolo de comunicação que elimina algumas restrições da composição paralela de processos na tradução para Handel-C, permitindo que a comunicação em um mesmo canal entre múltiplos processos possa ser mapeada de maneira consistente e que no código gerado não ocorra comunicações indevidas em um canal, ou seja, comunicações que não são permitidas na especificação do sistema.#$&Abstract: Removing inconsistencies in a project is a less expensive activity when done in the early steps of design. The use of formal methods improves the understanding of systems. They have various techniques such as formal specification and verification to identify these problems in the initial stages of a project. However, the transformation from a formal specification into a programming language is a non-trivial task and error prone, specially when done manually. The aid of tools at this stage can bring great benefits to the final product to be developed. This paper proposes the extension of a tool whose focus is the automatic translation of specifications written in CSPM into Handel-C. CSP is a formal description language suitable for concurrent systems, and CSPM is the notation used in tools support. Handel-C is a programming language whose result can be compiled directly into FPGA s. Our extension increases the number of CSPM operators accepted by the tool, allowing the user to define local processes, to rename channels in a process and to use Boolean guards on external choices. In addition, we also propose the implementation of a communication protocol that eliminates some restrictions on parallel composition of processes in the translation into Handel-C, allowing communication in a same channel between multiple processes to be mapped in a consistent manner and that improper communication in a channel does not ocurr in the generated code, ie, communications that are not allowed in the system specification.
format	Dissertação
author	Medeiros Júnior, Ivan Soares de. Oliveira, Marcel Vinicius Medeiros. Universidade Federal do Rio Grande do Norte.
author_facet	Medeiros Júnior, Ivan Soares de. Oliveira, Marcel Vinicius Medeiros. Universidade Federal do Rio Grande do Norte.
author_sort	Medeiros Júnior, Ivan Soares de.
title	Geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução /
title_short	Geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução /
title_full	Geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução /
title_fullStr	Geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução /
title_full_unstemmed	Geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução /
title_sort	geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução /
publishDate	2022
url	https://repositorio.ufrn.br/jspui/bitstream/123456789/18052/1/IvanSMJ_DISSERT.pdf
work_keys_str_mv	AT medeirosjuniorivansoaresde geracaoautomaticadehardwareapartirdeespecificacoesformaisestendendoumaabordagemdetraducao AT oliveiramarcelviniciusmedeiros geracaoautomaticadehardwareapartirdeespecificacoesformaisestendendoumaabordagemdetraducao AT universidadefederaldoriograndedonorte geracaoautomaticadehardwareapartirdeespecificacoesformaisestendendoumaabordagemdetraducao
_version_	1766835855510470656

Geração automática de hardware a partir de especificações formais : estendendo uma abordagem de tradução /

Registros relacionados