The Formal Mechanism of the UML Model Based on SBOPN

摘要

This paper introduces the State-Based Object Petri net, gives the definition, firing rule and analysis methods of the net. Based on aforementioned, state-based object petri net is chosen to formalize the UML and give the mechanism and corresponding algorithms that can be used to map state chart diagrams and the collaboration diagram of UML specification into state-based object petri net model in the early phase of UML modeling. The state-based object petri net 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 the verification of the model in the early phase is can be realized.