Menu Principal

Developed in conjunction with Ext-Joom.com

UFRN-DIMAp-2008-101-RT

Título: Verified compilation based on the B method: an initial appraisal (extended version)

Autores: Bartira Dantas, David Déharbe, Stephenson Galvão, Valério Medeiros Júnior, Anamaria Martins Moreira

Abstract: This report presents an application of the software engineering process known as the B method beyond the classical algorithmic level provided by the B0 sub-language, and presents refinements of B models in a level of precision equivalent to assembly language. We claim and justify that this extension provides for a more reliable software development process as it bypasses two of the less trustable steps in the application of the B method: code synthesis and compilation. The results presented in the paper have a value as a proof of concept and may be used as a basis to establish an agenda for the development of an approach to build verifying compilers [4] based on the B method.

Keywords: Software engineering; formal methods; B method; refinement; compilation.

Resumo: Esse relatório apresenta a aplicação do método B, um processo de engenharia de software, além do nível algorítmico tradicional provido pela sub-linguagem B0, e apresenta refinamentos de modelos B em um nível de precisão que equivale ao de uma linguagem de assemblagem. Afirmamos, e justificamos, que essa extensão resulte em um processo de desenvolvimento de software mais confiável pois elimina dois passos menos confiáveis na aplicação do método B: a síntese de código em linguagem de programação e a sua compilação. Os resultados apresentados têm valor como prova de conceito e são usados como base para estabelecer uma agenda para desenvolver uma abordagem de construção de compiladores verificadores [4] baseados no método B.

Palavras-Chave: Engenharia de software; métodos formais; o método B; refinamento; compilação.

Link para Download: UFRN-DIMAp-2008-101-RT

UFRN-DIMAp-2005-101-RT

Título: Anais do IV Workshop Técnico Científico do DIMAp

Resumo: Esse relatório técnico contém as contribuições acadêmicas que foram apresentadas no IV Workshop Técnico Científico do DIMAp, ocorrido em outubro de 2005.

Keywords: Computer Science

Abstract: This technical report contains the academic works presented at the IV technical and scientific workshop of DIMAp, which took place in October 2005.

Organizadores: Anamaria Martins Moreira, Umberto Souza da Costa, Pedro Fernandes Maia

Link para Download: UFRN-DIMAp-2005-101-RT