Formal Verification Of UML Statechart Based On Petri Nets

Unified Modeling Language (UML) is a generic visual modeling and specification language. UML provides an open method for system description, documentation and building object-oriented software intensive systems. However, UML has not been given a strict formal semantics, which can only describe a dynamic model without execution. This makes the verification of the model a problem. Therefore, it is difficult to identify bugs of a software system at the early stage of software development and design, which will lead to increased development costs. In contrast, a Petri net, with a sound theoretical basis and strict formal semantics, is an executable model. Based on the advantages of the two models, the paper converts a state diagram model of UML to a Petri net model, and achieves the purpose of ensuring the original model’s correctness and rationality through analysis of Petri nets model validation.This paper describes the current research literature both at home and abroad of the mapping between UML and Petri nets model, and then presents the basic theory of Petri nets.As the two models are graphical, the paper, initially proposes mapping rules based on the graphic model, and then proves the correctness of mapping rules in formal methods to ensure the equivalence of semantics. Upon the completion of mapping rules, the paper develops an automatic conversion tool of both models, and then introduces the workflow of the tool by demonstration of an instance.This paper, taking a Small Online Shopping System as an example, firstly designs use case diagram, class diagram, and order’s state diagram of the system based on VP-UML. Then the order’s state diagram is converted into Petri net model by using automatic conversion tool. Finally the paper analyses the property of the model and verifies the model’s behavior based on Petri Nets theory. This verifies the feasibility and correctness of the mapping method.The achievement and innovation of this paper is processing and presenting the formalization of the UML model in the way of executable models. This paper takes the way of transforming the UML model to Petri Nets model to formalize the UML, and ensures the correctness of the mapping rules in terms of theoretical proof and samples validation methods. The practical example of the Small Online Shopping System also shows the availability of the formalization in real software development. the formalization can improve the accuracy and reliability of the software system to a certain extent.