The Formalization Of UML Modeling

As a de facto standard of objected-oriented software modeling language, UML has succeeded in analysis and designs of many systems. However, it also has many flaws. Although the main part of UML syntax has been well defined, as well as the static semantics, the dynamic semantics is almost described in natural language. As a result, there is frequently ambiguity and vagueness in UML specifications. Therefore, the formal semantic study of UML is very helpful for the improvement of the clarification, equivalence, consistency, and extendibility of the language, thus offers a powerful theoretical tool for the validity proof, transition of the model and the consistency check of the modeling tools supporting UML.The forepart of this thesis is mainly about formal methods, OOZS and UML. OOZS is an objected-oriented formal specification language evolved from Z language. In the following part, four UML diagrams: class diagram, use case diagram, statechart diagram and sequence diagram are formalized using OOZS. That is, all model elements of these four diagrams are represented by its formal syntax and semantics. According to the above work, a mapping from non-formal model which is composed of graphs and letters to formal model based on mathematics is actually built. Further work includes model consistency checking, code autogeneration, test case autogeneration, program validity verification etc.