Método B e a síntese verificada para código de montagem
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 const...
Na minha lista:
| Autor principal: | |
|---|---|
| Outros Autores: | |
| Formato: | doctoralThesis |
| Idioma: | por |
| Publicado em: |
Brasil
|
| Assuntos: | |
| Endereço do item: | https://repositorio.ufrn.br/jspui/handle/123456789/21420 |
| Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|
| id |
ri-123456789-21420 |
|---|---|
| record_format |
dspace |
| institution |
Repositório Institucional |
| collection |
RI - UFRN |
| language |
por |
| topic |
Métodos formais Método B Tradução de modelos Verificação de tradução Linguagem de montagem CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO |
| spellingShingle |
Métodos formais Método B Tradução de modelos Verificação de tradução Linguagem de montagem CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO Medeiros Júnior, Valério Gutemberg de Método B e a síntese verificada para código de montagem |
| description |
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. |
| author2 |
Deharbe, David Boris Paul |
| author_facet |
Deharbe, David Boris Paul Medeiros Júnior, Valério Gutemberg de |
| format |
doctoralThesis |
| author |
Medeiros Júnior, Valério Gutemberg de |
| author_sort |
Medeiros Júnior, Valério Gutemberg de |
| title |
Método B e a síntese verificada para código de montagem |
| title_short |
Método B e a síntese verificada para código de montagem |
| title_full |
Método B e a síntese verificada para código de montagem |
| title_fullStr |
Método B e a síntese verificada para código de montagem |
| title_full_unstemmed |
Método B e a síntese verificada para código de montagem |
| title_sort |
método b e a síntese verificada para código de montagem |
| publisher |
Brasil |
| publishDate |
2016 |
| url |
https://repositorio.ufrn.br/jspui/handle/123456789/21420 |
| work_keys_str_mv |
AT medeirosjuniorvaleriogutembergde metodobeasinteseverificadaparacodigodemontagem |
| _version_ |
1773962461570924544 |
| spelling |
ri-123456789-214202017-11-03T06:45:20Z Método B e a síntese verificada para código de montagem Medeiros Júnior, Valério Gutemberg de Deharbe, David Boris Paul http://lattes.cnpq.br/7451897900811657 http://lattes.cnpq.br/2985658685449858 Musicante, Martin Alejandro http://lattes.cnpq.br/6034405930958244 Oliveira, Marcel Vinícius Medeiros http://lattes.cnpq.br/1756952696097255 Mota, Alexandre Cabral http://lattes.cnpq.br/2794026545404598 Gomes, Bruno Emerson Gurgel http://lattes.cnpq.br/7812661521592212 Métodos formais Método B Tradução de modelos Verificação de tradução Linguagem de montagem CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO 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. 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. 2016-10-14T20:28:33Z 2016-10-14T20:28:33Z 2016-03-08 doctoralThesis MEDEIROS JÚNIOR, Valério Gutemberg de. Método B e a síntese verificada para código de montagem. 2016. 138f. Tese (Doutorado em Ciência da Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2016. https://repositorio.ufrn.br/jspui/handle/123456789/21420 por Acesso Aberto application/pdf Brasil UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO |