Correctness, Completeness and Termination of Pattern-based Model-to-Model Transformation: Long Version | Publicación