In modern, computer-aided engineering processes, restoring and maintaining the consistency of multiple, related artefacts is an important challenge. This is especially the case in multi-disciplinary domains such as manufacturing engineering, where complex systems are described using multiple artefacts that are concurrently manipulated by domain experts, each with their own established tools. Bidirectional languages address this challenge of consistency maintenance by supporting incremental change propagation with a clear and precise semantics. Triple Graph Grammars (TGGs) are a prominent rule-based and declarative bidirectional model transformation language with various implementations, and a solid formal foundation based on algebraic graph transformations. Although TGGs are well suited for synchronizing models that are already on an appropriate, high-level of abstraction, practical model synchronization chains typically require handling models on different levels of abstraction. This poses additional challenges including: (i) handling massive information loss typically incurred when abstracting from a low-level model to a high-level model, (ii) supporting complex attribute manipulation as low-level models are often simple trees extracted from textual or XML-files, with relevant information encoded in attribute values rather than structural relations, and (iii) enabling arbitrary structural constraints to cope with complex, often recursive structural context relations, which are usually not present as explicit links in low-level models.

This thesis addresses these challenges by: (1) Establishing a general framework for organizing and structuring model synchronization chains. This framework is applied to an industrial case study in the domain of manufacturing engineering, which is used consequently throughout this thesis to identify requirements, formulate corresponding challenges, and evaluate the contributions of this thesis. (2) Identifying and formalizing new language extensions for TGGs: attribute conditions for complex attribute manipulation in TGG rules, and dynamic conditions for integrating arbitrary structural constraints. To guarantee the maintainability of large TGG specifications, a new modularity concept for TGGs, rule refinement is also introduced. Similar to inheritance and composition for programming languages, rule refinement enables the reuse and flexible combination of TGG rule fragments to form similar TGG rules without introducing redundancy in specifications. (3) Extending an existing TGG-based synchronization algorithm to cover these new features with formal proofs of correctness and completeness (well-behavedness) of derived TGG-based synchronizers. (4) Providing formal construction techniques and static analyses for all properties and restrictions required to guarantee the well-behavedness of derived synchronizers.