B Method Based Framework for Correct Software Development

In this paper, we proposed a lightweight framework for correctness of software development based on B formal method. The purpose of this framework is to transform requirement documents described by natural language to executable codes. During the process, at first, the elements and relations of the target system are acquired through natural language analysis from requirement documents. Then modules are elicited from the entities and relationship based on the composition clauses in B method, and then the elicited modules are described by B specification which can be refined into B implementation, and finally the B implementation is translated into executable codes. Moreover, the correctness of the final software is guaranteed through the analysis of each phase in the process.