Les architectures orientees services constituent l'un des principaux modeles architecturaux couramment utilises aujourd'hui. La propriete essentielle de ces architectures est le faible couplage entre les fournisseurs et les demandeurs de services. Cela permet de developper et de deployer les briques des applications de maniere independante. Ceci conduit a une grande dynamique de l'environnement d'execution ou les services peuvent apparaitre et disparaitre a tout moment. Cependant, cette dynamique des services souleve de nombreux defis, dont l'un des principaux est de pouvoir donner le maximum de garanties sur le fait qu'une application utilisant les services developpes par ailleurs s'executera comme prevu par ses concepteurs. Dans le present manuscrit, nous nous interessons a la substitution des services avec etat (stateful). Par ailleurs, prendre en compte les comportements des services dans le processus de decouverte permettrait d'effectuer un meilleur choix du service a substituer. Ce manuscrit s'addresse a tous ceux qui travaillent sur la substitution des services et des composants, et aussi a tous les passionnes des langages formels pour le genie logiciel."