What is the state of the art in theory of "Software transformations preserving behavior"? I am interested in the field that could perhaps be referred to as "Automated Refactory" or "Preservation of Software Properties" after a transformation/change/refactory.

Saying we have an instruction/set of instructions I with some functional property P and some transformation T so that I' = T(I). Is there any research/work/papers that models P (just some properties, a group of, ...) and preservation/changes of those properties between I and I' for a set of transformations T? 

First of all, what is the correct name for this fiels? Then, I would like to know if a theory to model this problem exists, which one is the most used (or the most referred to) and if any application of that system/metric/model (libraries, IDE plugins, ...) has been released.

If you can give any name, paper, ... whatever that is considered "fundamental" in this field, I will dig into this on my own.
I think what you are looking for, in the context of verified transformations in a proof assistant, is known as "refinement", wherein a very-high level, inefficient implementation of some algorithm is gradually refined down into an efficient, low-level implementation, proving that the transformations preserve certain properties along the way.  Various tools have been developed to help the user do this without being overcome by tedious book keeping.

In terms of the state of the art, I think Lammich's tool in Isabelle/HOL has been used successfully in at least two significant developments (a verification of Hopcroft's algorithm by Lammich and Tuerk, and a verified implementation of an LTL model checker by Esparza, Lammich et al).  Ironically, I was also reading this paper this morning, about a similar tool, newly developed, in Coq, courtesy of the dependent_types subreddit on Reddit.