Bridging the gap between formal semantics and implementation of triple graph grammars
- The correctness of model transformations is a crucial element for 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 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 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. While 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 showThe correctness of model transformations is a crucial element for 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 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 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. While 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 and runtime checks can be employed to guarantee these criteria.…
Author details: | Holger GieseORCiDGND, Stephan Hildebrandt, Leen LambersORCiDGND |
---|---|
DOI: | https://doi.org/10.1007/s10270-012-0247-y |
ISSN: | 1619-1366 |
ISSN: | 1619-1374 |
Title of parent work (English): | Software and systems modeling |
Publisher: | Springer |
Place of publishing: | Heidelberg |
Publication type: | Article |
Language: | English |
Year of first publication: | 2014 |
Publication year: | 2014 |
Release date: | 2017/03/27 |
Volume: | 13 |
Issue: | 1 |
Number of pages: | 27 |
First page: | 273 |
Last Page: | 299 |
Funding institution: | Deutsche Forschungsgemeinschaft |
Organizational units: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science |
Peer review: | Referiert |
Institution name at the time of the publication: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik |