A Verification Method of UML Model Based on SBOPN

This paper introduces the State-Based Object Petri Net (SBOPN), and based on aforementioned, we choose SBOPN to formalize the UML and gave 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 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.