Proposal and Evaluation of a Trustworthy Software Development Approach by Construction Using the B Method
Abstract
This work describes a model-driven approach to design and develop software from the functional specification level down to assembly. The proposed approach builds upon the B method and provides a methodology to craft assembly-level software components in a rigorous way. While the B method is conventionally applied to produce algorithmic level software artifacts for safety-critical systems, it was not originally designed to handle the final transformations to source code and then to assembly. The users of the B method need thus to use code synthesis and compilation tools that do not offer the same rigorousness. Subtle bugs in these final steps may indeed jeopardize the whole engineering process. The approach proposed in the paper extends the B method to covers these last steps and therefore contributes to the scientific grand challenge of Computer Science proposed by Tony Hoare [6]: “The Verifying Compiler”.
References
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.
