Code Generation from B Specification based on Component Oriented Approach

In this paper we propose a framework for code generation from B formal specification based on component based method. First, software components can be derived form B abstract machines according to their relativity. Then, by using proved translation rules the elicited software components are translated into code directly. Finally, all the software components are assembled into a whole system with correct assembly rules. The trustworthiness of generated code is insured by the correctness of B abstract machines and the assembly strategies. Component based approach is used to ease complex verification among different B abstract machines and it also facilitates the software reuse.