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.
Maria Semenyak