Code mobility technologies attract more and more developers and consumers. Numerous domains are concerned, many platforms are developed and interest applications are realized. However, developing good software products requires modeling, analyzing and proving steps. The choice of models and modeling languages is so critical on these steps. Formal tools are powerful in analyzing and proving steps. However, poorness of classical modeling language to model mobility requires proposition of new models. The objective of this paper is to provide a formal approach based on LRN and R-Maude. LRN (Labeled Reconfigurable Nets) is a specific formalism that we propose to model different kinds of code mobility. R-Maude (Reconfigurable Maude) is a system that we devlop to encode and simulate LRN-models.