Skip to main content
Erschienen in: Software and Systems Modeling 4/2014

01.10.2014 | Regular Paper

Colouring: execution, debug and analysis of QVT-relations transformations through coloured Petri nets

verfasst von: Esther Guerra, Juan de Lara

Erschienen in: Software and Systems Modeling | Ausgabe 4/2014

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

QVT is the standard language sponsored by the OMG to specify model-to-model transformations. It includes three different languages, being QVT-relations (QVT-R) the one with higher-level of abstraction. Unfortunately, there is scarce tool support for it nowadays, with incompatibilities and disagreements between the few tools implementing it, and lacking support for the analysis and verification of transformations. Part of this situation is due to the fact that the standard provides only a semi-formal semantics for QVT-R. In order to alleviate this situation, this paper provides a semantics for QVT-R through its compilation into coloured Petri nets. The theory of coloured Petri nets provides useful techniques to analyse transformations (e.g. detecting relation conflicts, or checking whether certain structures are generated or not in the target model) as well as to determine their confluence and termination given a starting model. Our semantics is flexible enough to permit the use of QVT-R specifications not only for transformation and check-only scenarios, but also for model matching and model comparison, not covered in the original standard. As a proof of concept, we report on the use of CPNTools for the execution, debugging, verification and validation of transformations, and on a tool chain (named Colouring) to transform QVT-R specifications and their input models into the input format of CPNTools, as well as to export and visualize the transformation results back as models.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
For simplicity, by now we intentionally avoid using class inheritance in the meta-models. We will show how our method handles inheritance in Sect. 4.6.
 
2
CPNTools depicts enabled transitions by highlighting them in green colour.
 
3
The purpose of this somewhat artificial example is to show the effect of the CBE semantics in Sects. 4.5 and 7.
 
4
A2 stores objects of type A, but we use a different name because CPNTools does not allow duplicated place names in the same page.
 
5
Currently, our generator does not consider CBE semantics or optimizations of places. This is left as future work.
 
6
Modelink is part of the GMT Epsilon project, available at http://​www.​eclipse.​org/​epsilon/​doc/​modelink/​.
 
7
MediniQVT does not prevent these queries and may produce target models that together with the source one would not pass the check-only scenario.
 
Literatur
1.
Zurück zum Zitat Barkaoui, K., Dutheillet, C., Haddad, S.: An efficient algorithm for finding structural deadlocks in colored Petri nets. In: APN’93, pp. 69–88 (1993) Barkaoui, K., Dutheillet, C., Haddad, S.: An efficient algorithm for finding structural deadlocks in colored Petri nets. In: APN’93, pp. 69–88 (1993)
3.
Zurück zum Zitat Boronat, A., Carsí, J.A., Ramos, I.: Algebraic specification of a model transformation engine. In: FASE’06. LNCS, vol. 3922, pp. 262–277. Springer, Berlin (2006) Boronat, A., Carsí, J.A., Ramos, I.: Algebraic specification of a model transformation engine. In: FASE’06. LNCS, vol. 3922, pp. 262–277. Springer, Berlin (2006)
4.
Zurück zum Zitat Boronat, A., Heckel, R., Meseguer, J.: Rewriting logic semantics and verification of model transformations. In: FASE’09. LNCS, vol. 5503, pp. 18–33. Springer, Berlin (2009) Boronat, A., Heckel, R., Meseguer, J.: Rewriting logic semantics and verification of model transformations. In: FASE’09. LNCS, vol. 5503, pp. 18–33. Springer, Berlin (2009)
5.
Zurück zum Zitat Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. J. Syst. Softw. 83(2), 283–302 (2010)CrossRef Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. J. Syst. Softw. 83(2), 283–302 (2010)CrossRef
6.
Zurück zum Zitat Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured Petri nets exploiting strongly connected components. In: WODES’96, pp. 169–177 (1996) Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured Petri nets exploiting strongly connected components. In: WODES’96, pp. 169–177 (1996)
7.
Zurück zum Zitat Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999) Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
8.
Zurück zum Zitat Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude—A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Berlin (2007) Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude—A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Berlin (2007)
10.
Zurück zum Zitat de Lara, J., Guerra, E.: Formal support for QVT-Relations with coloured Petri nets. In: MoDELS’09. LNCS, vol. 5795, pp. 256–270. Springer, Berlin (2009) de Lara, J., Guerra, E.: Formal support for QVT-Relations with coloured Petri nets. In: MoDELS’09. LNCS, vol. 5795, pp. 256–270. Springer, Berlin (2009)
11.
Zurück zum Zitat Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer, Berlin (2006)MATH Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer, Berlin (2006)MATH
12.
Zurück zum Zitat Evangelista, S., Haddad, S., Pradat, J.-F.: Syntactical colored Petri nets reductions. In: ATVA’05. LNCS, vol. 3707, pp. 202–216. Springer, Berlin (2005) Evangelista, S., Haddad, S., Pradat, J.-F.: Syntactical colored Petri nets reductions. In: ATVA’05. LNCS, vol. 3707, pp. 202–216. Springer, Berlin (2005)
14.
Zurück zum Zitat García, M.: Formalization of QVT-Relations: OCL-based static semantics and alloy-based validation. In: MDSD Today, pp. 21–30. Shaker Verlag (2008) García, M.: Formalization of QVT-Relations: OCL-based static semantics and alloy-based validation. In: MDSD Today, pp. 21–30. Shaker Verlag (2008)
15.
Zurück zum Zitat Greenyer, J., Kindler, E.: Comparing relational model transformation technologies: implementing Query/View/Transformation with triple graph grammars. Softw. Syst. Model. 9(1), 21–46 (2010) Greenyer, J., Kindler, E.: Comparing relational model transformation technologies: implementing Query/View/Transformation with triple graph grammars. Softw. Syst. Model. 9(1), 21–46 (2010)
16.
Zurück zum Zitat Guerra, E., de Lara, J., Orejas, F.: Inter-modelling with patterns. Softw. Syst. Model (2011, in press) Guerra, E., de Lara, J., Orejas, F.: Inter-modelling with patterns. Softw. Syst. Model (2011, in press)
17.
Zurück zum Zitat Heckel, R., Küster, J.M., Taentzer, G.: Confluence of typed attributed graph transformation systems. In: ICGT. LNCS, vol. 2505, pp. 161–176. Springer, Berlin (2002) Heckel, R., Küster, J.M., Taentzer, G.: Confluence of typed attributed graph transformation systems. In: ICGT. LNCS, vol. 2505, pp. 161–176. Springer, Berlin (2002)
18.
Zurück zum Zitat Jensen, K.: Coloured Petri Nets Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science. Springer, Berlin (1997) Jensen, K.: Coloured Petri Nets Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science. Springer, Berlin (1997)
19.
Zurück zum Zitat Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. STTT 9(3–4):213–254 (2007). http://cpntools.org. Accessed July 2011 Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. STTT 9(3–4):213–254 (2007). http://​cpntools.​org. Accessed July 2011
22.
Zurück zum Zitat Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I., Valduriez, P.: ATL: a QVT-like transformation language. In: OOPSLA’06, pp. 719–720. ACM, New York (2006) Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I., Valduriez, P.: ATL: a QVT-like transformation language. In: OOPSLA’06, pp. 719–720. ACM, New York (2006)
24.
Zurück zum Zitat Kolovos, D.S.: Establishing correspondences between models with the Epsilon Comparison Language. In: ECMDA-FA’09. LNCS, vol. 5562, pp. 146–157. Springer, Berlin (2009) Kolovos, D.S.: Establishing correspondences between models with the Epsilon Comparison Language. In: ECMDA-FA’09. LNCS, vol. 5562, pp. 146–157. Springer, Berlin (2009)
25.
Zurück zum Zitat Kolovos, D.S., Paige, R.F., Polack, F.: Merging models with the Epsilon Merging Language (EML). In: MoDELS’06. LNCS, vol. 4199, pp. 215–229. Springer, Berlin (2006) Kolovos, D.S., Paige, R.F., Polack, F.: Merging models with the Epsilon Merging Language (EML). In: MoDELS’06. LNCS, vol. 4199, pp. 215–229. Springer, Berlin (2006)
26.
Zurück zum Zitat Kolovos, D.S., Paige, R.F., Polack, F.: The Epsilon Transformation Language. In: ICMT’08. LNCS, vol. 5063, pp. 46–60. Springer, Berlin (2008) Kolovos, D.S., Paige, R.F., Polack, F.: The Epsilon Transformation Language. In: ICMT’08. LNCS, vol. 5063, pp. 46–60. Springer, Berlin (2008)
27.
Zurück zum Zitat Kolovos, D.S., Ruscio, D.D., Pierantonio, A., Paige, R.F.: Different models for model matching: an analysis of approaches to support model differencing. In: CVSM’09, pp. 1–6. IEEE CS (2009) Kolovos, D.S., Ruscio, D.D., Pierantonio, A., Paige, R.F.: Different models for model matching: an analysis of approaches to support model differencing. In: CVSM’09, pp. 1–6. IEEE CS (2009)
28.
Zurück zum Zitat Königs, A., Schürr, A.: Tool integration with triple graph grammars: a survey. ENTCS 148(1), 113–150 (2006) Königs, A., Schürr, A.: Tool integration with triple graph grammars: a survey. ENTCS 148(1), 113–150 (2006)
29.
30.
Zurück zum Zitat Lucas, F.J., Álvarez, J.A.T.: Model transformations powered by rewriting logic. In: CAiSE Forum. CEUR Proceedings, vol. 344, pp. 41–44 (2008) Lucas, F.J., Álvarez, J.A.T.: Model transformations powered by rewriting logic. In: CAiSE Forum. CEUR Proceedings, vol. 344, pp. 41–44 (2008)
32.
Zurück zum Zitat Mellor, S.J., Scott, K., Uhl, A., Weise, D.: MDA Distilled. Addison-Wesley Object Technology Series (2004) Mellor, S.J., Scott, K., Uhl, A., Weise, D.: MDA Distilled. Addison-Wesley Object Technology Series (2004)
35.
Zurück zum Zitat Ohta, A., Tsuji, K.: On some analysis properties of colored Petri net using underlying net. In: MWSCAS’04, vol. 3, pp. 395–398. IEEE CS (2004) Ohta, A., Tsuji, K.: On some analysis properties of colored Petri net using underlying net. In: MWSCAS’04, vol. 3, pp. 395–398. IEEE CS (2004)
36.
Zurück zum Zitat Petter, A., Behring, A., Mühlhäuser, M.: Solving constraints in model transformations. In: ICMT’09. LNCS, vol. 5563, pp. 132–147. Springer, Berlin (2009) Petter, A., Behring, A., Mühlhäuser, M.: Solving constraints in model transformations. In: ICMT’09. LNCS, vol. 5563, pp. 132–147. Springer, Berlin (2009)
38.
Zurück zum Zitat Romeikat, R., Roser, S., Müllender, P., Bauer, B.: Translation of QVT relations into QVT operational mappings. In: ICMT’08. LNCS, vol. 5063, pp. 137–151. Springer, Berlin (2008) Romeikat, R., Roser, S., Müllender, P., Bauer, B.: Translation of QVT relations into QVT operational mappings. In: ICMT’08. LNCS, vol. 5063, pp. 137–151. Springer, Berlin (2008)
39.
Zurück zum Zitat Schürr, A.: Specification of graph translators with triple graph grammars. In: WG’94. LNCS, vol. 903, pp. 151–163. Springer, Berlin (1994) Schürr, A.: Specification of graph translators with triple graph grammars. In: WG’94. LNCS, vol. 903, pp. 151–163. Springer, Berlin (1994)
41.
Zurück zum Zitat Stahl, T., Volter, M.: Model-Driven Software Development: Technology, Engineering, Management. Wiley, New York (2006) Stahl, T., Volter, M.: Model-Driven Software Development: Technology, Engineering, Management. Wiley, New York (2006)
43.
Zurück zum Zitat Stevens, P.: A simple game-theoretic approach to checkonly QVT relations. Softw. Syst. Model (2012, in press) Stevens, P.: A simple game-theoretic approach to checkonly QVT relations. Softw. Syst. Model (2012, in press)
44.
Zurück zum Zitat van Amstel, M., Bosems, S., Kurtev, I., Pires, L.F.: Performance in model transformations: experiments with ATL and QVT. In: ICMT’11. LNCS, vol. 6707, pp. 198–212. Springer, Berlin (2011) van Amstel, M., Bosems, S., Kurtev, I., Pires, L.F.: Performance in model transformations: experiments with ATL and QVT. In: ICMT’11. LNCS, vol. 6707, pp. 198–212. Springer, Berlin (2011)
45.
Zurück zum Zitat Wimmer, M., Kappel, G., Schönböck, J., Kusel, A., Retschitzegger, W., Schwinger, W.: A Petri net based debugging environment for QVT relations. In: ASE’09, pp. 3–14. IEEE CS (2009). http://www.modeltransformation.net/. Accessed Nov 2010 Wimmer, M., Kappel, G., Schönböck, J., Kusel, A., Retschitzegger, W., Schwinger, W.: A Petri net based debugging environment for QVT relations. In: ASE’09, pp. 3–14. IEEE CS (2009). http://​www.​modeltransformat​ion.​net/​. Accessed Nov 2010
Metadaten
Titel
Colouring: execution, debug and analysis of QVT-relations transformations through coloured Petri nets
verfasst von
Esther Guerra
Juan de Lara
Publikationsdatum
01.10.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 4/2014
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-012-0292-6

Weitere Artikel der Ausgabe 4/2014

Software and Systems Modeling 4/2014 Zur Ausgabe