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