Toward bridging the gap between formal semantics and implementation of triple graph grammars

  • The correctness of model transformations is a crucial element for the model-driven engineering of high quality software. A prerequisite to verify model transformations at the level of the model transformation specification is that an unambiguous formal semantics exists and that the employed implementation of the model transformation language adheres to this semantics. However, for existing relational model transformation approaches it is usually not really clear under which constraints particular implementations are really conform to the formal semantics. In this paper, we will bridge this gap for the formal semantics of triple graph grammars (TGG) and an existing efficient implementation. Whereas the formal semantics assumes backtracking and ignores non-determinism, practical implementations do not support backtracking, require rule sets that ensure determinism, and include further optimizations. Therefore, we capture how the considered TGG implementation realizes the transformation by means of operational rules, define requiredThe correctness of model transformations is a crucial element for the model-driven engineering of high quality software. A prerequisite to verify model transformations at the level of the model transformation specification is that an unambiguous formal semantics exists and that the employed implementation of the model transformation language adheres to this semantics. However, for existing relational model transformation approaches it is usually not really clear under which constraints particular implementations are really conform to the formal semantics. In this paper, we will bridge this gap for the formal semantics of triple graph grammars (TGG) and an existing efficient implementation. Whereas the formal semantics assumes backtracking and ignores non-determinism, practical implementations do not support backtracking, require rule sets that ensure determinism, and include further optimizations. Therefore, we capture how the considered TGG implementation realizes the transformation by means of operational rules, define required criteria and show conformance to the formal semantics if these criteria are fulfilled. We further outline how static analysis can be employed to guarantee these criteria.show moreshow less

Download full text files

Export metadata

Additional Services

Search Google Scholar Statistics
Metadaten
Author details:Holger GieseORCiDGND, Stephan Hildebrandt, Leen LambersORCiDGND
URN:urn:nbn:de:kobv:517-opus-45219
ISBN:978-3-86956-078-6
Publication series (Volume number):Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam (37)
Publisher:Universitätsverlag Potsdam
Place of publishing:Potsdam
Publication type:Monograph/Edited Volume
Language:English
Publication year:2010
Publishing institution:Universität Potsdam
Release date:2010/08/26
Number of pages:26
RVK - Regensburg classification:ST 230
Organizational units:An-Institute / Hasso-Plattner-Institut für Digital Engineering gGmbH
DDC classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Publishing method:Universitätsverlag Potsdam
License (German):License LogoKeine öffentliche Lizenz: Unter Urheberrechtsschutz
Accept ✔
This website uses technically necessary session cookies. By continuing to use the website, you agree to this. You can find our privacy policy here.