Made available in DSpace on 2014-12-17T15:47:56Z (GMT). No. of bitstreams: 1 SAMUEL LINCOLNdissertacao_final.pdf: 2269762 bytes, checksum: f3ae8e1d8966bfbf455c79b080c96cc2 (MD5) Previous issue date: 2011-08-29 / This dissertation aims at extending the JCircus tool, a translator of formal specifications into code that receives a Circus specification as input, and translates the specification into Java code. Circus is a formal language whose syntax is based on Z s and CSP s syntax. JCircus generated code uses JCSP, which is a Java API that implements CSP primitives. As JCSP does not implement all CSP s primitives, the translation strategy from Circus to Java is not trivial. Some CSP primitives, like parallelism, external choice, communication and multi-synchronization are partially implemented. As an aditional scope, this dissertation will also develop a tool for testing JCSP programs, called JCSPUnit, which will also be included in JCircus new version. The extended version of JCircus will be called JCircus 2.0. / Esta disserta??o tem como objetivo estender a ferramenta JCircus, um tradutor de especifica??es formais para c?digo que recebe uma especifica??o em Circus como entrada, e traduz a especifica??o para c?digo Java. Circus ? uma linguagem formal cuja sintaxe ? baseada nas sintaxes das linguagens Z e CSP. O c?digo gerado por JCircus faz uso de JCSP, que ? uma API de Java que implementa primitivas de CSP. O fato de JCSP n?o implementar CSP completamente faz com que a estrat?gia de tradu??o de Circus para Java seja n?o-trivial. Algumas primitivas de CSP, como paralelismo, escolhas externa e interna, comunica??o, e multi-sincroniza??o s?o implementadas em JCSP de forma parcial. Nesta disserta??o, estendemos a tradu??o destas primitivas. Al?m disso, esta disserta??o tamb?m desenvolver? uma ferramenta para fazer testes em processos JCSP, chamada JCSPUnit.