Design of ATL Rules for Transforming UML 2 Sequence Diagrams into Petri Nets

Abstract

UML  2 sequence  diagrams  are  a  well-known graphical  language and  are  widely used  to  specify the  dynamic  behaviors  of transaction-oriented systems.   However, sequence diagrams are expressed in a semi-formal modeling language and need a well-defined formal semantic base for their notations. This formalization enables analysis and verification tasks.   Many efforts have been made to transform sequence diagrams into formal representations including Petri Nets.  Petri Nets are a mathematical tool allowing formal specification of the system dynamics and they are commonly used in Model Checking.   In this paper, we present a transformation approach that consists of a source metamodel for UML 2 sequence diagrams, a target metamodel for Petri Nets and transformation rules.  This approach has been implemented using Atlas Transformation Language (ATL).  A Cellular Phone System is considered, as a case study.

Keywords

UML 2, Sequence diagrams, Petri Nets, Model checking, Model transformation, Metamodeling, Transformation rules, ATL