Formal Foundations for Information-Preserving Model Synchronization Processes Based on Triple Graph Grammars