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!
|
| Resumo: | 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. |
|---|