The Verification Of UML Model Based On SBOPN

As a standard modeling language of object-oriented methodology, UML is interface-friendly, expressive, powerful and popular, but it is not a formalized modeling language and is lack of exactly semantic description so that it is difficult to analyze and verify in the early phase of designing the UML model. As a modeling tool, the Petri net is able to not only give the effective and formalizing model of the distributed and concurrent procedure, but also present strictly mathematic analysis and instinct computer-simulation to the structure and the dynamic behavior of the system, so it is selected to formalize the UML model.This paper introduces the State-Based Object Petri Net (SBOPN), gives the definition, firing rule and analysis methods of the net and discusses the object-oriented feature of it. Based on aforementioned, we choose SBOPN to formalize the UML and give the mechanism and corresponding algorithms that can be used to map statechart diagrams and collaboration diagram of UML specification into SBOPN model in the early phase of UML modeling. The SBOPN model gotten by these algorithms not only is object-oriented but also can be analyzed and validated to find out deadlock with powerful Petri tools, thus we can realize the verification of the model in the early phase . We illustrate the method through the oven system and ATM machine that are first specified by UML and then mapped into corresponding SBOPN model. Meanwhile, using the reachable marking graph model, we analyze and validate SBOPN model of the spacecraft flying control system derived with its UML model. Then, the tool's prototype of the UML model verification based on SBOPN is given. Finally we present the future research orientation of the topic.