Research And Application Of Formal Method In Automatic Code Generation

Since the reform and opening up,the computer field has also entered a stage of rapid development,which has brought great changes to people.In the future,computer-based research and development applications will accelerate the development of society.The generation of automatic code tools can greatly liberate people's hands and further improve the efficiency of software development.However,as the scale and complexity of development systems continue to increase,the error rate of software development increases.How to improve the accuracy of requirements description and code consistency in the early stage of software development has become more and more important,and has become a hot spot in the field of software engineering research.The Unified Modeling Language(UML)is the most widely used visual modeling language in object-oriented technology.It is well defined,easy to build,and documented.However,the semi-structured UML model lacks formal semantics,and it is difficult to analyze and verify it using mathematical methods.It is difficult to judge the integrity and correctness of the model.Therefore,in the automatic code generation process,the formal description of the precise semantics and analysis of the UML model is particularly important.The formal method was born in the 1950 s.The technology based on strict mathematics has a very significant effect on improving the correctness of software systems.It is the most rigorous method in software development today.Based on the unified modeling language UML and the formal method theory,this paper adds the formal method to the automatic code generation process.This makes the semantic representation of the UML model more precise and the generated code more representative.This paper studies the theory and examples of formal transformation of UML model diagrams,improves the transformation rules of UML models to formal methods,and formulates the transformation rules between formal methods and object-oriented language Java code.This article mainly does the following work:(1)Firstly,the theory of UML and B formalization methods is analyzed,because the UML semantics under natural language description is not accurate enough.The B formalization method provides an unambiguous and more accurate description of the software system.The combination of the two has a positive effect on improving the reliability of the software.(2)Based on the detailed analysis of UML state chart model and B abstract machine symbol,this paper studies the existing theory of formal transformation of UML model.Then through the mapping relationship between the UML model and the B formalization method,the transformation rules from the UML state diagram to the B abstract machine are improved.(3)In the code generation phase,the mapping rules between the B formalization method and the object-oriented language Java are formulated.(4)Complete the programming of the automatic generation tool,and implement the model conversion implementation tool on the Eclipse development platform using the Java language.And through the case to verify that the method proposed in this paper is effective and feasible.