¹Department of Computer Science, University of Oum El Bouaghi, Algeria
²MISC Laboratory, Department of Computer Science, University of Constantine, Algeria
³University of Bourgogne, LE2I Laboratoire, Dijon, France

---

Abstract—The use of the UML specification language for modelling dynamic behaviors of systems is very widespread. UML Statecharts and Collaboration diagrams are widely used to model dynamic behaviors of systems. However, the lack of firm semantics for the UML modeling notations makes the detection of behavioral inconsistencies difficult in the initial phases of development. The use of formal methods makes such error detection possible but the learning cost is high. Integrating UML with a suitable formal notation is a promising approach that makes UML more precise and amenable to rigorous analysis. In this paper, we present the benefits of a similar approach that is the integration of UML Statechart and Collaboration diagrams and Colored Petri Nets models. The result is an automated approach and a tool environment that formally transforms dynamic behaviors of systems expressed using UML models into their equivalent Colored Petri Nets models for analysis purposes. To make the analysis easier, the obtained models are used to generate automatically their equivalent description in the input language of the INA Petri net analyzer. The approach is based on Graph Transformation and the Meta-Modeling tool ATOM3 is used. The approach is illustrated through an example.

Index Terms—UML; CPN; INA Analyzer; Meta-Modeling; Graph Grammars; Graph Transformation; Models Transformation; AToM3.

[PDF]

Cite: Elhillali Kerkouche, Allaoua Chaoui, El Bay Bourennane, Ouassila Labbani, "On the Use of Graph Transformation in the Modeling and Verification of Dynamic Behavior in UML Models," Journal of Software vol. 5, no. 11, pp. 1279-1291, 2010.