This chapter has shown the formal definitions of the transformations for Rosa's system. The formal definition is quite long and far from trivial; every detail needs to be correct. It is a time-consuming task to write it, and a good tool for checking the consistency is required. However, we must realize that without applying MDA, these kinds of transformations have always been executed by hand and not automated nor well defined. After the formalization is completed, it can be used many times in many projects and the payback can be huge.