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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/21420 |
| Date | 08 March 2016 |
| Creators | Medeiros J?nior, Val?rio Gutemberg de |
| Contributors | 00809085437, http://lattes.cnpq.br/2985658685449858, Musicante, Martin Alejandro, 82500304434, http://lattes.cnpq.br/6034405930958244, Oliveira, Marcel Vin?cius Medeiros, 02386943488, http://lattes.cnpq.br/1756952696097255, Mota, Alexandre Cabral, 73547735491, http://lattes.cnpq.br/2794026545404598, Gomes, Bruno Emerson Gurgel, 01061676420, http://lattes.cnpq.br/7812661521592212, Deharbe, David Boris Paul |
| Publisher | PROGRAMA DE P?S-GRADUA??O EM SISTEMAS E COMPUTA??O, UFRN, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| 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.0024 seconds