The Research Form UML Modeling To Z Formal Specification

Along with the computer’s performance continues to improve, people increasingly want more and more difficult problem for computers to solve. The scale of software system is larger and larger, increasing complexity. However, the possibility of software error increases. The reports about disastrous consequences because of a software error are many. In the case of increasing software complexity, how to ensure the quality of the software, to improve the reliability of the software, has caused great concern in the field of software engineering research.Unified Modeling Language (UML) is now a more mature modeling language, a wide range of use of software development. UML supports object-oriented analysis and design, and provides a lot of the basic representation of model elements of the graphical method, the expression of a variety of object-oriented concepts and model elements can be clear and concise manner, it is able to describe the software, visual processing, structure and the establish the documentation of the software system. UML model as a graphical language, it is clear that the logical model and representation model of the system, it has powerful skills so that it can be used for a variety of complex software systems modeling. But the UML has also the problem of the lack of precise semantics, not concise enough, there is ambiguity difficult to verify the correctness of the results.Formal methods of software development based on rigorous mathematical development method can accurately unambiguous description of the system, and it has strict proof. Z language is a formal language in the industry of "state actions" style, which is based on first-order predicate logic and set theory, using a collection of mathematical concepts such as relations, functions, sequences and package. It uses state mode and operation mode to descript the state and behavior of the target system, with a concise and precise. Z language has been widely used in industry and academia, and has been called the "software engineering language".In this paper, we combine the Unified Modeling Language (UML) and Z language. The formal description of the Unified Modeling Language (UML) class diagrams based on the Z language is proposed. By this method we improve the quality of a system specification, using the integrated UML-Z prototype system UML-Z tool to achieve the conversion from UML class diagrams to the Z language specification, there are some basic operation automatically converted, proof and verification model. This method ensures that the quality of the software system, and improves the reliability of the software system, so it is feasible.