Made available in DSpace on 2014-12-17T15:48:01Z (GMT). No. of bitstreams: 1 IvanSMJ_DISSERT.pdf: 2894212 bytes, checksum: 3acb921ac87239ee36be60cb2e15b0e6 (MD5) Previous issue date: 2012-04-27 / 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. 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 a 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. 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 entre m?ltiplos processos possa ser mapeada de maneira consistente e que a mesma somente ocorra quando for autorizada.