M. Wimmer, G. Kappel, A. Kusel, W. Retschitzegger, J. Schönböck, W. Schwinger: Right or Wrong? - Verification of Model Transformations using Colored Petri Nets, in Proceedings of the 9th OOPSLA Workshop on Domain-Specific Modeling (DSM´09), Helsinki Business School, 2009, Paper-Nr. 15. pdf
Model-Driven Engineering (MDE) places models as firstclass artifacts throughout the software lifecycle requiring the availability of proper transformation languages. Most of today’s approaches use declarative rules to specify a mapping between source and target models which is then executed by a transformation engine. Transformation engines, however, most often hide the operational semantics of the mapping and operate on a considerable lower level of abstraction, thus hampering debugging. To tackle these limitations we propose a framework called TROPIC (Transformations on Petri Nets in Color) providing a DSL on top of Colored Petri Nets (CPNs) to specify, simulate, and formally verify model transformations. The formal underpinnings of CPNs enables simulation and veri fication of model transformations. By exploring the constructed state space of CPNs we show how prede fined behavioral properties as well as custom state space functions can be applied for observing and tracking
origins of errors during debugging.