Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-10-11T20:48:08Z No. of bitstreams: 1 ValerioGutembergDeMedeirosJunior_TESE.pdf: 1793475 bytes, checksum: 151ab0c6b194c17a043978ff9682034b (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-10-14T20:28:32Z (GMT) No. of bitstreams: 1 ValerioGutembergDeMedeirosJunior_TESE.pdf: 1793475 bytes, checksum: 151ab0c6b194c17a043978ff9682034b (MD5) / Made available in DSpace on 2016-10-14T20:28:33Z (GMT). No. of bitstreams: 1 ValerioGutembergDeMedeirosJunior_TESE.pdf: 1793475 bytes, checksum: 151ab0c6b194c17a043978ff9682034b (MD5) Previous issue date: 2016-03-08 / A s?ntese de c?digo de montagem ? um processo que exige um cuidado rigoroso. Normalmente, esse processo nos tradutores e nos compiladores mais maduros ? relativamente seguro, apesar de que, esporadicamente, erros s?o identificados neles. Em um contexto mais restrito, os tradutores utilizados em comunidades menores e em constante desenvolvimento s?o mais suscet?veis a erros. Considerando esse contexto, duas abordagens de tradu??o e de verifica??o usando o m?todo B s?o apresentadas. A primeira abordagem prop?e a tradu??o do componente B para o c?digo de montagem de uma plataforma espec?fica, usando um modelo formal do conjunto de instru??es, o qual possibilita tamb?m depurar e verificar as propriedades de programas. Essa abordagem ? capaz de garantir formalmente a coer?ncia sem?ntica da tradu??o, apesar de ser um processo de verifica??o ?rduo e lento. Tal esfor?o de verifica??o foi aliviado atrav?s de uma ferramenta desenvolvida (BEval), que aproveitou melhor as t?cnicas de verifica??o. Ap?s o processo de prova autom?tica usando uma ferramenta B robusta (Atelier B), BEval ainda foi capaz de resolver em certos modelos muitas das obriga??es de prova remanescentes, chegando a at? 88% do total de obriga??es. Contudo, o processo de verifica??o da abordagem de tradu??o continuou complexo, exigindo v?rias intera??es manuais. Afim de viabilizar uma tradu??o mais eficiente e tamb?m segura, uma segunda abordagem de tradu??o de B para o c?digo de m?quina virtual foi desenvolvida. A segunda abordagem utilizou o tradutor desenvolvido B2LLVM e aplicou a gera??o autom?tica de testes para verificar a coer?ncia entre a especifica??o do programa e o seu respectivo c?digo de montagem. Esse tradutor tamb?m suporta a avalia??o de cobertura do c?digo e a inser??o de anota??es de rastreabilidade. Dessa forma, o trabalho contribuiu significativamente na tradu??o de B para o c?digo de montagem, oferecendo um suporte rigoroso para a verifica??o da tradu??o. Atualmente, o B2LLVM j? ? capaz de gerar c?digo para 84% dos exemplos de teste baseados na gram?tica que s?o traduz?veis por um relevante tradutor industrial (C4B). Ademais, o c?digo gerado por B2LLVM apresenta vantagens importantes na ampla capacidade de verifica??o, de integra??o e de otimiza??o. / Assembly code synthesis is a process that requires rigorous care. Typically, this process in mature translators and compilers is relatively safe, though some errors have occasionally been identified. In a more restricted context, the translators used in the smaller communities and developed constantly have been more susceptible to these kind of errors. Considering this context, two translation and verification approaches using the B method have been presented. The first approach considers the B component translation to assembly code for a specific platform by using a formal model of the instruction set, which also allows to debug and to check program properties. This approach can formally ensure the semantic consistency of the translation, although the verification process is difficult and time-consuming. This verification effort was somewhat relieved by the development of BEval, a tool which has made better use of the verification techniques. After applying the automatic verification process using the Atelier B tool, BEval was still able to solve, in the certain models, many of the remaining proof obligations, reaching up to 88 % of total obligations. However, the verification process of this translation approach is still complex, requiring several manual interactions. In order to make a translation more efficient and also safe, a second approach for the translating B to virtual machine code was developed. This second approach used the developed translator B2LLVM and applied the automatic generation of tests to check the consistency of the program specifications and their respective assembly code. This translator also supported the code coverage evaluation and the insertion of the traceability annotations. Thus, this study has significantly contributed to developing B translation to assembly code, providing rigorous support for the verification of the translation. Currently, the B2LLVM outweighs 20,9% the percentage of translatable test samples based on grammar compared to the C4B industrial translator. Furthermore, the generated code by B2LLVM has important advantages in the ample capacity of verification, integration and optimization.