L’analyse d’accessibilité est une des composantes de l’analyse de modèles. Elle consiste à modéliser un système complexe par trois ensembles : le langage initial, le langage des configurations indésirables et un système de réécriture. Le langage initial et le langage des configurations indésirables sont des ensembles de termes. Un terme est un mot mais construit à partir de symboles d’arités supérieures à 1. Le système de réécriture représente la dynamique du système complexe. C’est un ensemble de règles qui permettent d’obtenir un nouveau terme à partir d’un terme original. Pour effectuer une analyse d’accessibilité à partir de cette modélisation, on peut calculer l’ensemble des configurations accessibles. Cet ensemble aussi appelé ensemble des descendants est obtenu en appliquant le système de réécriture sur le langage initial jusqu’à ne plus obtenir de nouveaux termes. Une fois l’ensemble des descendants calculé, il reste à faire l’intersection entre celui-ci et l’ensemble des configurations indésirables. Si cette intersection est vide, alors il n’y a pas de configuration indésirable accessible, sinon les configurations présentes dans cette intersection sont accessibles. Cependant, l’ensemble des descendants n’est pas calculable dans le cas général. Pour contourner ce problème, nous calculons une sur-approximation des descendants. Ainsi, si l’intersection est vide, cela signifie toujours qu’aucune configuration indésirable n’est accessible. A contrario, s’il existe un terme dans l’intersection, il n’est pas possible de déterminer s’il s’agit d’un faux positif ou d’une configuration indésirable accessible. La précision de la sur-approximation est alors déterminante. / Reachability analysis is part of model checking. It consists to model complex systems by three sets : initial language, unwanted configurations and rewrite system. The initial language and the unwanted configurations language are sets of terms. Terms are words which are construct with symbols that have an arity that can be greater than 1. The rewrite system represent the dynamic of the complex system. It is a set of rules that permit from a initial term to obtain a new term. One of the approaches to analyze reachability from this modelling is to compute the set of reachable configurations. This set which is called set of descendants is obtained by applying the rewrite system on the initial language until obtaining no more new terms. After the set of descendants is computed, we need to compute the intersection between this set and the unwanted configurations set. If this intersection is empty then there is no unwanted configuration reachable, else the configurations in this intersection are reachable. However, the set of descendants is not computable in the general case. To bypass this problem, we compute an over-approximation of descendants.Now, if the intersection is empty, we keep proving that no unwanted configuration is reachable. Nevertheless, if the intersection is not empty, it is not possible to know if it comes from false-positives or form unwanted reachable configurations. So, the precision of the over-approximation is decisive.

La plupart des processus informatiques mettent en jeu la notion de transformation, en particulier la compilation. Nous nous intéressons dans cette thèse à fournir des outils et des méthodes, utilisant la réécriture, permettant d'accroître la confiance que l'on peut placer dans ces processus. Nous développons dans un premier temps un cadre permettant de valider la compilation de constructions de filtrage, produisant une preuve formelle de la validité de la compilation, ainsi qu'un témoin de cette preuve, à chaque exécution du compilateur. Afin de permettre l'écriture sûre de transformations complexes, nous proposons un générateur de structures de données efficaces intégrant des invariants algébriques, et un langage de stratégies permettant de contrôler l'application des transformations. Ces résultats constituent donc une avancée vers la constitution de methodes génériques sûres pour le développement de transformations de confiance. / Most computer processes involve the notion of transformation, in particular the compilation processes. We interest in this thesis in providing tools and methods, based on rewriting, giving the opportunity to increase the confidence we can place into those processes. We develop first a framework used to validate the compilation of matching constructs, building a formal proof of the validity of the compilation process along with a witness of this proof, for each run of the compiler. Then, in order to allow one to write safely complex transformations, we propose a tool that generates an efficient data structure integrating algebraic invariants, as well as a strategy language that enables to control the application of transformations. Those results can be seen as a first step towards the constitution of generic and safe methods for the development of trustworthy transformations.