The Formalization Of UML Modeling And Its Application

Unified Modeling language (UML) supports Object-Oriented analysis and design. UML offering a set of basic graphic and method to describe modeling elements, it can depict modeling element concisely and clearly. We use UML to describe software, to built files for the construction of software system. UML is a visual language. Its model diagrams may indicate the logical model and implementation model of the system. The strong expression makes it possible that UML can make model for kinds of complex software system. But, there are some flaws of UML, such as scarce of precise semantic ambiguous of verification and so on.Formal Method has strict mathematical foundations and strict verifications. It can describe system precisely. B-method is a useful formal method of software development. It includes all the process from abstract verification to execute code. B-method use Abstract Machine Notation (AMN) construct requirement model. B-method supports the test of category and dynamic verification of specification. The tools supporting B use animation to simulate the function of specification. According to the test of demands and scenario, it can tell whether the specification is satisfied by users.The organic combination of UML and B-method not only conserves the advantages of UML in constructing model. But also make up for the flaws of UML. B-method provides concise semantic reference of UML models. It can eliminate the inconsistency among kinks of UML models. Simultaneously, it reduce the degree of difficulties of using B-method directly. The combination ensures the quality of software, and enhances the accuracy and effect of software development.The forepart of this thesis is mainly about the mathematical foundations of B-method and the theory of AMN. The following part introduces UML simply. The main part is about how to describe UML class diagram and state diagram by using B-method. During the process of software development, the developer builds models of target system firstly, then transmit the models to B-method verification, and use tools of B-method to analysis or check these models, as a correct beginning of formal refinement.The last part gives an application of order management system which is the most important component of logistics management. Firstly, construct the UML class diagram and state diagram of order system. Secondly, implement the B-method description of the UML model. Lastly, gives the test of model...