A Formal Analysis Method And Its Application Based On UML Requirement Modeling

Software requirement analysis is the first work in the software development process. Whether its analysis result is accurate and reliable will affect the quality of the software products directly, even will determine whether the project succeeds or not. Moreover, the method of requirement analysis has become a key factor in the improvement of its quality and even the quality of the final software products.UML is a widely used modeling language in the software development process. However, it is a semi-formal modeling language which lacks precise semantics. So, on one hand, it is hard for the software requirement models modeled by UML to precisely describe user's requirement semantics; on the other hand, it is difficult to directly verify and refine these models, and even harder to improve the correctness and reliability of software. So, UML needs to be expanded in formalization.This paper is aimed to discuss a method on how to formalize requirement modeling based on UML by Object-Z and Perfect. The key point is to formalize the syntax and static semantics of UML Class Diagram of UML metamodel by Object-Z, and to explore a mapping and transforming mechanism between the metamodels of UML and Object-Z, then to establish a mapping between the metamodels of Object-Z and Perfect, followed by defining some translation rules for their mapping, so that Object-Z specifications can be refined and verified by Perfect. Thus, not only can it retain the strong modeling capability and concise object-oriented model representation while we are analyzing and designing system by UML, but also it can formalize, refine and verify the requirement models modeled by UML. It can further illustrate the feasibility of actual application of the method through the formalized description and refinement of the requirement models of the enterprise personnel system and the automated checking system modeled by UML.To conclude, by combining UML, Object-Z and Perfect, we can obtain a new descriptive method of software requirement which can better meet such needs as the analysis, design and development of software system whose scale and complexity are on the rise, and can help improving the correctness and reliability of software to a certain extent.