Colored Petri Net Model Based On UML And Its Application In ICONIX

UML is one kind of full-featured visible modeling language with strong versatility, but it cannot support formal verification and analysis because of lacking accurate semantic expressions. At present, there are several researches pertaining to UML formalization. Some directly define UML model into formal semantics, and then analyze UML model with formal semantics and do correctness verification; others transfer UML model into specification with precise semantics and formalization. But most of research results have limitations. In the several researches, using Petri Net theory to do UML formalization verification is a good choice, firstly, Petri Net has its own perfect and reliable theory analysis methods, which contains formalization principle with accurate semantics, can supplement the weakness that UML lacks model verification analysis; moreover, Petri Net, as a graphical demonstrated model, is strongly intuitive that is beneficial for analysis; finally, Petri Net has mature analysis tool, CPN tools, which can run effective and quick analysis after transition from UML to Petri Net, software developer without strong math basics also can use this to formally analyze UML,In the practical software development, a suited software developing process is significant, this paper did not choose RUP, which we are familiar with, but use ICONIX that is between heavyweight RUP and lightweight XP to develop software, since RUP is to theoretical and require strictly for UML definition. Because this pare mainly illustrate one kind of method to transfer UML graph into colored Petri Net, and ICONIX do a certain amount choice based extensible UML, which can decrease complexity of UML transformation, as well as its supreme robustness and traceability, so we realize ICONIX. ICONIX mostly includes sequential graph and class graph, in previous research of UML and Petri Net, there are research results, and for example, sequential graph, status graph, class graph and other UML graphs respectively transfer into Petri Net. The conversion method is transferring class graph and sequential graph into colored Petri Net model together, this conversion combine static information of class graph and dynamic information of sequential graph, which leads UML formalization analysis more accurate. First step is combine sequential graph and class graph into an equivalent intermediate graph, named pseudo class graph; Second step is converting the intermediate graph into colored Petri Net to generate executable model based on colored Petri Net, using analysis tool, CPN tools to simulate analysis, and realize the UML formalization in ICONIX.