Research On Formalization Of UML Based On Petri Net

With Object-oriented technology developing, many object-oriented modeling language appeared, the Unified Modeling Language (UML) as a powerful graphical and well-defined modeling language is widely used. UML Combines new ideas and new technologies of the software engineering, supports the whole process of software's development from the software requirements analysis to completion. It has become the actual industry standard. However, as the software size and complexity are continuous increasing, System modeling is required to improve. Modeling complex systems requires rigorous formal analysis and verification can guarantee the correctness of the system, while the UML syntax using the formal statute, but semantic used natural language, the lack of accuracy, the model is difficult to establish the dynamic analysis and verification. With the improvement of software quality requirements, Research on Formalization of UML gets more and more attention.In this paper, I consider the character that UML has graphical description; use the Petri net system as a formal specification, avoiding difficult limitations of the directly use formal specification methods for modeling. As Petri net and UML are graphical modeling tools, it can more easily combine the advantages of both. Compared with the UML system model, The Petri net can characterize the structure and describe the dynamic behavior of the system. Petri net not only have intuitive graphical representation, but also have a solid, rigorous mathematical foundation, with many sophisticated methods of analysis can be directly used to analyze the performance of the model. In this paper, UML state diagram and UML sequence diagram are converted to Petri net model. The UML sequence diagram is extended expressive power, the introduction of concurrency, synchronization, select the three special message passing system, to describe the operation of system better.For the establishment of formal Petri net model using the reachability tree algorithm, analysis reachable, security, activity and other dynamic features of Petri net models, to improve the UML model and improve software quality. This paper improves constructing the reachability tree algorithm, defines the data structure, reduces storage space and computational complexity, and improves the efficiency of Petri net model's analysis.This article describes Anhui Agricultural Insurance System meteorological services business formal UML modeling in detail and analysis process. Agricultural Insurance System is converted to formal Petri model and this model is analyzed. The automated analysis tools based on the reachability tree algorithm of Petri net is developed.