Skip to main content
SpringerLink
Log in

Formal Support for QVT-Relations with Coloured Petri Nets

  • Conference paper
Model Driven Engineering Languages and Systems (MODELS 2009)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5795))

Abstract

QVT is the OMG standard language for specifying model-to-model transformations in MDA. Even though it plays a crucial role in model driven development, there are scarce tools supporting the execution of its sublanguage QVT-Relations, and none for its analysis or verification. In order to alleviate this situation, this paper provides a formal semantics for QVT-Relations through its compilation into Coloured Petri nets, enabling the execution and validation of QVT specifications. The theory of Petri nets provides useful techniques to analyse transformations (e.g. reachability, model-checking, boundedness and invariants) and to determine their confluence and termination given a starting model. We also report on using CPNTools for the execution, debugging, and analysis of transformations, and on a tool chain to transform QVT-Relations specifications into the input format of CPNTools.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Boronat, A., Carsí, J.A., Ramos, I.: Algebraic specification of a model transformation engine. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 262–277. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  2. Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: An invariant-based method for the analysis of declarative model-to-model transformations. In: Czarnecki, K., Ober, I., Bruel, J.-M., Uhl, A., Völter, M. (eds.) MODELS 2008. LNCS, vol. 5301, pp. 37–52. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured petri nets exploiting strongly connected components. In: WODES, pp. 169–177 (1996)

    Google Scholar 

  4. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of algebraic graph transformation. Springer, Heidelberg (2006)

    MATH  Google Scholar 

  5. Evangelista, S., Haddad, S., Pradat, J.-F.: Syntactical colored petri nets reductions. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 202–216. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. García, M.: Formalization of QVT-Relations: OCL-based static semantics and Alloy-based validation. In: MDSD today, pp. 21–30. Shaker Verlag (2008)

    Google Scholar 

  7. Greenyer, J.: A study of model transformation technologies: Reconciling TGGs with QVT. Master’s thesis, University of Paderborn (2006)

    Google Scholar 

  8. Jensen, K.: Coloured Petri nets basic concepts, analysis methods and practical use (Monographs in theoretical computer science). Springer, Heidelberg (1997)

    Google Scholar 

  9. 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://wiki.daimi.au.dk/cpntools

    Article  Google Scholar 

  10. JET (2009), http://www.eclipse.org/modeling/m2t/?project=jet

  11. Lucas, F.J., Álvarez, J.A.T.: Model transformations powered by rewriting logic. In: CAiSE Forum. CEUR Proc., vol. 344, pp. 41–44 (2008)

    Google Scholar 

  12. MediniQVT (2009), http://projects.ikv.de/qvt/

  13. ModelMorf (2009), http://www.tcs-trddc.com/ModelMorf/index.htm

  14. Ohta, A., Tsuji, K.: On some analysis properties of colored petri net using underlying net. In: MWSCAS 2004, vol. 3, pp. 395–398. IEEE, Los Alamitos (2004)

    Google Scholar 

  15. QVT (2005), http://www.omg.org/docs/ptc/05-11-01.pdf

  16. Strommer, M., Wimmer, M.: A framework for model transformation by-example: Concepts and tool support. In: TOOLS. LNBIP, vol. 11, pp. 372–391. Springer, Heidelberg (1974)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad Autónoma de Madrid, Spain

    Juan de Lara

  2. Universidad Carlos III de Madrid, Spain

    Esther Guerra

Authors
  1. Juan de Lara
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Esther Guerra
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fachgebiet Echtzeitsysteme, Technische Universität Darmstadt, Merckstraße 25, 64283, Darmstadt,, Germany

    Andy Schürr

  2. Malina Software Corporation, 10 Blueridge Court, Nepean,, K2J 2J3, Ontario, Canada

    Bran Selic

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Lara, J., Guerra, E. (2009). Formal Support for QVT-Relations with Coloured Petri Nets. In: Schürr, A., Selic, B. (eds) Model Driven Engineering Languages and Systems. MODELS 2009. Lecture Notes in Computer Science, vol 5795. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04425-0_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04425-0_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04424-3

  • Online ISBN: 978-3-642-04425-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation