@Article{ Giese+2014,
  AUTHOR = {Giese, Holger and Hildebrandt, Stephan and Lambers, Leen},
  TITLE = {{Bridging the Gap between Formal Semantics and Implementation
  of Triple Graph Grammars - Ensuring Conformance of Relational Model
  Transformation Specifications and Implementations}},
  YEAR = {2014},
  JOURNAL = {Software and Systems Modeling},
  VOLUME = {13},
  NUMBER = {1},
  PAGES = {273-299},
  PUBLISHER = {Springer Berlin Heidelberg},
  URL = {http://dx.doi.org/10.1007/s10270-012-0247-y},
  ABSTRACT = {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 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.}
}