Proposta e Avaliação de uma Abordagem de Desenvolvimento de Software Fidedigno por Construção com o Método B

• B. Dantas UFRN
• D. Déharbe UFRN
• S. Galvão UFRN
• A. Martins Moreira UFRN
• V. Medeiros Júnior UFRN

Resumo

O artigo descreve uma abordagem orientada a modelos para o desenvolvimento de componentes de software abrangendo desde a especificação funcional até a produção de código em nível de montagem. A abordagem proposta tem como base o método B e permite projetar e construir componentes de software em assembly de forma rigorosa e comprovadamente correta. Enquanto o método B é tradicionalmente aplicado pela indústria para desenvolver componentes de software para sistemas críticos até um nível algorítmico, ele não foi originalmente concebido para tratar das últimas transformações até a geração de código de montagem ou executável. A abordagem proposta nesse artigo estende o método B para cobrir essas últimas transformações e dessa forma contribui para uma das metas do Grande Desafio 5 que é o “desenvolvimento e adaptação de tecnologias e instrumentos em geral de apoio à implementação e à avaliação de software fidedigno por construção”.

Referências

Grandes Desafios da Pesquisa em Computação no Brasil: 2006–2016. [link], 2006. Sociedade Brasileira de Computação.

R. Abrial. The B-Book: Assigning programs to meanings. Cambridge Univ. Press, 1996.

A. Cavalcanti, A. Sampaio, and J. Woodcock. Procedures and recursion in the refinement calculus. Journal of the Brazilian Computer Society, 5(1):5–19, 1998.

A. Cavalcanti, A. Sampaio, and J. Woodcock. A refinement strategy for circus. Formal Aspects of Computing, 15(2–3):147–181, 2003.

B. Dantas, D. Déharbe, S. Galvão, V. Medeiros Jr, and A. Moreira. Verified compilation based on the B method: an initial appraisal (extended version). Technical Report UFRN-DIMAp-2008-101-RT, UFRN-DIMAp, 2008.

C. A. R. Hoare. The verifying compiler, a grand challenge for computing research. In VMCAI, pages 78–78, 2005.

J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison Wesley, 1979.

E. Jaffuel and B. Legeard. LEIRIOS test generator: Automated test generation from B models. In The 7th International B Conference, pages 277–280, 2007.

C. B. Jones. Systematic Software Development Using VDM. Prentice Hall Int., 1990.

P. Letouzey. A new extraction for Coq. In TYPES 2002, volume 2646 of LNCS, 2003.

D. Ossami, J.-P. Jacquot, and J. Souquières. Consistency in UML and B multi-view specifications. In IFM, pages 386–405, 2005.

C.Y Park. Predicting program execution times by analyzing static and dynamic program paths. Real-Time Systems, 5(1):31–61, 1993.

S. Schneider. The B-Method: An Introduction. Cornerstones of Computing Series. Palgrave, 2001.

C. Snook and M. Butler. UML-B: Formal modelling and design aided by UML. ACM Transactions on Software Engineering and Methodology, 15(1):92–122, 2006.

J. Spivey. The Z Notation: a Reference Manual. Prentice-Hall International Series in Computer Science. Prentice Hall, 2nd edition, 1992.