Toward Bridging the Gap Between Formal Semantics and Implementation of Triple Graph Grammars (bibtex)
Reference:
Holger Giese, Stephan Hildebrandt and Leen Lambers, "Toward Bridging the Gap Between Formal Semantics and Implementation of Triple Graph Grammars", Technical Report 37, Hasso Plattner Institute at the University of Potsdam, 2010.
Abstract:
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 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.
Links:
@TechReport{GieseHildebrandtLambers2010_1,
AUTHOR = {Giese, Holger and Hildebrandt, Stephan and Lambers, Leen},
TITLE = {{Toward Bridging the Gap Between Formal
Semantics and Implementation of Triple Graph
Grammars}},
YEAR = {2010},
NUMBER = {37},
INSTITUTION = {Hasso Plattner Institute at the University of Potsdam},
URL = {https://publishup.uni-potsdam.de/frontdoor/index/index/docId/4415},
OPTacc_url = {},
PDF = {uploads/pdf/GieseHildebrandtLambers2010.pdf},
OPTacc_pdf = {},
ABSTRACT = {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 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.}
}
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
Powered by bibtexbrowser