Transformation of UML Models into Analyzable OSAN Models

The unified modelling language (UML) is a de facto standard for object-oriented modelling. However, the formal semantics for the notations included in UML are not provided, which are a key requirement for the verification and evaluation purposes. To solve this problem, Petri net formalism has been used as a complement to UML in several research projects. However, there is not a complete transformation technique for all concepts and diagrams of UML to an extension of Petri nets. We have recently introduced object stochastic activity networks (OSANs). OSANs are a high-level modelling formalism that integrates object-orientation into stochastic activity networks (SANs). In this paper, we present some transformation techniques for the most important concepts and diagrams of UML into OSANs. The resulting OSAN models can be used for both evaluation and verification purposes.