Formal Transformation from Sequence Diagrams to Coloured Petri Nets

In this paper we define a formal strongly consistent transformation from UML2 sequence diagrams to coloured Petri nets (CPNs). We define the language of sequence diagrams (set of legal traces) and show how this is mapped onto an equivalent language of CPNs through formal transformation rules. The rules defined can be extended to consider modelling aspects such as stochastic and real-time behaviour. This work is part of a more general framework based on model driven transformations to validate UML models using Petri nets, and hence exploit existing Petri net analysis and verification tools for UML-based design.