Transformation of Activity Diagram into Coloured Petri Nets Using Weighted Directed Graph

摘要

UML Activity Diagram offers rich notations to model system dynamics of any real world system. But Activity Diagram lacks firm mathematical semantics hence impotent to be checked for potential inconsistencies and bugs. Coloured Petri Nets is a strong graphical Formal Methods having a wide range of tool support for model checking. This research article presents a new transformation strategy from Activity Diagram into its semantically equivalent Coloured Petri Nets using Weighted Directed Graph. The Activity Diagram is firstly transformed into a Weighted Directed Graph and in second step Weighted Directed Graph is transformed into semantically equivalent Coloured Petri Nets preserving the logic of all Activity Diagram constructs. The mapping of each Activity Diagram notations into its corresponding Coloured Petri Net construct has been semantically verified. Therefore, transformed Coloured Petri Nets can be checked for errors and inconsistencies by using any model checking tool of Coloured Petri Nets.