Flexible subtyping relations for component-oriented formalisms and their verification

In this thesis we address the problem of safe substitutability in mobile component-oriented formalisms. We try to give a solution for different definitions of "safe" through a new notion of subtyping based on flexibility and observation. The aim is to have a definition which is applicable to a large numbers of existing formalisms, and which itself may be seen as an abstraction of many existing definitions of subtyping. In a similar way, we also try to see the verification of such relations in a way that may be applicable to many formalisms, and which may be seen as "containing" many existing techniques. Our hope is that our work may link these subtype definitions or verification techniques to formalisms they were not originally designed for. The contribution of this thesis can be divided in several points. First of all, the full formal definition of a "descriptive" component-oriented formalism based on concurrency, non determinism, complex composition and mobility. Also, the definition of a general flexible notion of subtyping, as well as a more particular example. Verification techniques for these subtyping relations are also grouped under the concept of component transformation, which is shown to include many other works. Finally, to illustrate the main concepts of our work, we provide a case study with a model of a "mobile" drinks dispenser.