Modelltransformationen spielen eine Schlüsselrolle in automatisierten Software-Entwicklungsprozessen. Der moderne Trend geht in Richtung Spezifikation der Softwaremit einem abstrakten Modell und dessen schrittweiser Verwandlung zum Programmiercode.Es ist sehr wichtig, dass der Programmiercode der ursprünglichenSpezifikation entspricht. Deswegen ist eine wichtige Frage einer solchen Modelltransformation,ob das transformierte Modell die Verhaltenseigenschaften des Ausgangsmodellserfüllt. In dieser Doktorarbeit wird eine neue Methode für die Spezifikation von einerModelltransformation entwickelt und es wird gezeigt, dass die zu Grunde gelegte Modelltransformation korrekt ist.

Model transformations play a key role in automated software development processes,where the modern trend is directed towards specification of software with an abstractmodel and its step-wise transformation into code. It is important that the codemeets the initial specification. Therefore, the question for a model transformationis whether the transformed model fulfills the behavioural properties of the initialmodel. In this thesis, a method is presented for proving that a specified model transformationis semantically correct in the sense that it preserves all behavioural properties of a source model.