Skip to main content

Semantical Correctness and Completeness of Model Transformations Using Graph and Rule Transformation

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5214))

Abstract

An important requirement of model transformations is the preservation of the behavior of the original model. A model transformation is semantically correct if for each simulation run of the source system we find a corresponding simulation run in the target system. Analogously, we have semantical completeness, if for each simulation run of the target system we find a corresponding simulation run in the source system.

In our framework of graph transformation, models are given by graphs, and graph transformation rules are used to define the operational behavior of visual models (called simulation rules). In order to compare the semantics of source and target models, we assume that in both cases operational behavior can be defined by simulation rules. The model transformation from source to target models is given by another set of graph transformation rules. These rules are also applied to the simulation rules of the source model. The main result in this paper states the conditions for model and rule transformations to be semantically correct and complete. The result is applied to analyze the behavior of a model transformation from a domain-specific visual language for production systems to Petri nets.

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

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Narayanan, A., Karsai, G.: Using Semantic Anchoring to Verify Behavior Preservation in Graph Transformations. In: Proc. Workshop on Graph and Model Transformation (GraMoT 2006). EC-EASST, EASST, vol. 4 (2006)

    Google Scholar 

  2. Ermel, C.: Simulation and Animation of Visual Languages based on Typed Algebraic Graph Transformation. PhD thesis, Technische Universität Berlin,fak, IV, Books on Demand, Norderstedt (2006)

    Google Scholar 

  3. Ermel, C., Ehrig, H., Ehrig, K.: Semantical Correctness of Simulation-to-Animation Model and Rule Transformation. In: Proc. Workshop on Graph and Model Transformation (GraMoT 2006). EC-EASST, vol. 4, EASST (2006)

    Google Scholar 

  4. Ermel, C., Ehrig, H.: Behavior-preserving simulation-to-animation model and rule transformation. In: Proc. Workshop on Graph Transformation for Verification and Concurrency (GT-VC 2007). ENTCS, vol. 213(1), pp. 55–74. Elsevier Science, Amsterdam (2008)

    Google Scholar 

  5. Ehrig, H., Ermel, C.: Semantical Correctness and Completeness of Model Transformations using Graph and Rule Transformation: Long Version. Technical Report 2008-13, TU Berlin (2008), http://iv.tu-berlin.de/TechnBerichte/2008/2008-13.pdf

  6. de Lara, J., Vangheluwe, H.: Translating Model Simulators to Analysis Models. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 77–92. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  7. Lara, J., Bardohl, R., Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Attributed Graph Transformation with Node Type Inheritance. Theoretical Computer Science 376(3), 139–163 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  8. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. EATCS Monographs in Theor. Comp. Science. Springer, Heidelberg (2006)

    MATH  Google Scholar 

  9. Kreowski, H.-J.: A Comparison between Petri Nets and Graph Grammars. In: Noltemeier, H. (ed.) WG 1980. LNCS, vol. 100, pp. 1–19. Springer, Heidelberg (1981)

    Google Scholar 

  10. Ehrig, H., Ehrig, K.: Overview of Formal Concepts for Model Transformations based on Typed Attributed Graph Transformation. In: Proc. Workshop on Graph and Model Transformation (GraMoT 2005). ENTCS, vol. 152. Elsevier, Amsterdam (2005)

    Google Scholar 

  11. Varró, D.: Automated formal verification of visual modeling languages by model checking. Software and System Modeling 3(2), 85–113 (2004)

    Article  Google Scholar 

  12. Schürr, A.: Specification of Graph Translators with Triple Graph Grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol. 903, pp. 151–163. Springer, Heidelberg (1995)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ehrig, H., Ermel, C. (2008). Semantical Correctness and Completeness of Model Transformations Using Graph and Rule Transformation. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds) Graph Transformations. ICGT 2008. Lecture Notes in Computer Science, vol 5214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87405-8_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-87405-8_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-87404-1

  • Online ISBN: 978-3-540-87405-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics