Made available in DSpace on 2014-12-17T15:48:02Z (GMT). No. of bitstreams: 1
IvanSMJ_DISSERT.pdf: 2894212 bytes, checksum: 3acb921ac87239ee36be60cb2e15b0e6 (MD5)
Previous issue date: 2012-04-27 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / 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 / 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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/18052 |
| Date | 27 April 2012 |
| Creators | Medeiros Junior, Ivan Soares de |
| Contributors | CPF:02386943488, http://lattes.cnpq.br/1756952696097255, Mota, Alexandre Cabral, CPF:73547735491, http://lattes.cnpq.br/2794026545404598, Kreutz, M?rcio Eduardo, CPF:58434296049, http://lattes.cnpq.br/6374279398246756, Oliveira, Marcel Vinicius Medeiros |
| Publisher | Universidade Federal do Rio Grande do Norte, Programa de P?s-Gradua??o em Sistemas e Computa??o, UFRN, BR, Ci?ncia da Computa??o |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0028 seconds