Nous étudions des classes d'automates à états finis calculant sur les arbres, étendus par des contraintes permettant de tester des égalités et diségalités entre sous-arbres. Nous nous concentrons sur des automates d'arbres à contraintes globales où les tests sont opérés en fonction des états que l'automate atteint lors de ses calculs. De tels automates ont été introduit dans le cadre de travaux sur les documents semi-structurés. Nous procédons ici à une comparaison détaillée en expressivité entre ces automates et d'autres modèles permettant de réaliser des tests similaires, comme les automates à contraintes entre frères ou les automates d'arbres avec une mémoire auxiliaire. Nous montrons comment de tels automates peuvent être utilisés pour vérifier des propriétés de sécurité sur les protocoles cryptographiques. Les automates d'arbres ont déjà été utilisés pour modéliser les messages échangés lors d'une session d'un protocole. En ajoutant des contraintes d'égalité, nous pouvons décrire précisement des sessions qui utilisent à plusieurs reprises un même message, évitant ainsi une approximation trop grande. Nous répondons ensuite positivement au problème de la décision du vide des langages reconnus par les automates à contraintes globales. En montrant que leur expressivité est très proche de celle des automates opérant sur des représentations de termes par des graphes orientés acycliques, nous en déduisons une procédure de décision du vide en temps non-déterministe doublement exponentiel. Finalement, nous étudions le problème de la décision du vide pour des automates à contraintes globales pour lesquels on autorise des contraintes dites de clé, exprimant intuitivement que tous les sous arbres d'un certain type dans un arbre en entrée sont distincts deux à deux. Le type des clés est classiquement utilisé pour représenter un identifiant unique, comme un numéro de sécurité sociale.Nous décrivons alors une procédure de décision du vide de complexité non-élementaire. Nous montrons que cette procédure est très robuste, et qu'il est possible d'étendre les automates avec des contraintes supplémentaires, comme des contraintes de comptage ou des tests locaux, tout en préservant la décidabilité du vide.

Les automates d'arbres et leurs applications à la vérification forment le tronc commun de cette thèse. Dans la première parie, nous définissons une plate forme de model-checking complète [...] La seconde partie se penche sur un aspect important des automates que nous utilisons: leur contraintes [...] Finalement, nous étudions également les automates d'arbres cheminants [...] Nous améliorons leur conversion en automates parallèles, et nous développons une procédure de semi décision de leur vacuité, à la fois efficace et précise / Tree automata, and their applications to verification from the common thread of this thesis In the first part, we definie a complete model-cheking framework.[...] The second part focus on an important aspect of the automata involved: constraints.[...] Finaly, we also study the very different variety of tree-walking automata which have tight connections with navigational languages on semi-structured documents.

Nous nous intéressons par le problème de la sémantique des mises à jour et de la cohérence des bases de données dans différents contextes comme les documents XML et les services web. En effet, des difficultés particulières sont à prévoir lors de la mise à jour d'une base ayant des contraintes à respecter, car, des données originalement cohérentes par rapport aux contraintes peuvent devenir incohérentes suite aux mises à jour. Dans une première partie de notre travail, nous considérons la mise à jour et le maintien de la cohérence d'une base de données XML par rapport au type (ou schéma) ainsi que par rapport aux contraintes d'intégrité. Nous abordons ce problème de différentes manières. Tout d'abord, nous proposons une procédure de validation incrémentale par rapport aux contraintes, évitant de revalider les parties du document qui n'ont pas été touchées par les mises à jour. Cette approche traite aussi bien le cas des contraintes de schéma que le cas des contraintes d'intégrité. Dans ce cadre, les listes de mises à jour qui violent la validité sont rejetées. Quand la validation incrémentale échoue, c'est-à-dire, quand une mise à jour viole le type, deux propositions de traitement sont faites\,: (A) Une routine de correction est activée pour adapter le document XML au type tout en prenant en compte la mise à jour. La mise à jour a donc une priorité par rapport aux données déjà stockées. (B) Une routine propose une adaptation du type du document, de façon à accepter le document mis à jour en préservant la validité des autres documents originalement valides et non soumis à la mise à jour. Dans ce cas, la mise à jour est prioritaire et les contraintes peuvent être modifiées. Une deuxième partie du travail considère la construction d'une plate-forme d'aide à la spécification, à l'implémentation et à la manipulation de services. L'idée de pouvoir spécifier et modifier des compositions de services nous a amené à la définition du langage PEWS (\textit{Path Expressions for Web Services}), ayant une sémantique formelle bien définie et permettant la spécification du comportement des interfaces des services web simples ou composés. Pour pouvoir tester statiquement des propriétés liées à la composition des services, nous proposons l'utilisation de la théorie des traces et les graphes de dépendances.

Nous étudions des classes d'automates à états finis calculant sur les arbres, étendus par des contraintes permettant de tester des égalités et diségalités entre sous-arbres. Nous nous concentrons sur des automates d'arbres à contraintes globales où les tests sont opérés en fonction des états que l'automate atteint lors de ses calculs. De tels automates ont été introduit dans le cadre de travaux sur les documents semi-structurés. Nous procédons ici à une comparaison détaillée en expressivité entre ces automates et d'autres modèles permettant de réaliser des tests similaires, comme les automates à contraintes entre frères ou les automates d'arbres avec une mémoire auxiliaire. Nous montrons comment de tels automates peuvent être utilisés pour vérifier des propriétés de sécurité sur les protocoles cryptographiques. Les automates d'arbres ont déjà été utilisés pour modéliser les messages échangés lors d'une session d'un protocole. En ajoutant des contraintes d'égalité, nous pouvons décrire précisement des sessions qui utilisent à plusieurs reprises un même message, évitant ainsi une approximation trop grande. Nous répondons ensuite positivement au problème de la décision du vide des langages reconnus par les automates à contraintes globales. En montrant que leur expressivité est très proche de celle des automates opérant sur des représentations de termes par des graphes orientés acycliques, nous en déduisons une procédure de décision du vide en temps non-déterministe doublement exponentiel. Finalement, nous étudions le problème de la décision du vide pour des automates à contraintes globales pour lesquels on autorise des contraintes dites de clé, exprimant intuitivement que tous les sous arbres d'un certain type dans un arbre en entrée sont distincts deux à deux. Le type des clés est classiquement utilisé pour représenter un identifiant unique, comme un numéro de sécurité sociale.Nous décrivons alors une procédure de décision du vide de complexité non-élementaire. Nous montrons que cette procédure est très robuste, et qu'il est possible d'étendre les automates avec des contraintes supplémentaires, comme des contraintes de comptage ou des tests locaux, tout en préservant la décidabilité du vide. / We study here several classes of finite state automata running on trees, extended with constraints that allow to test for equalities or disequalities between subterms. We focus on tree automata with global constraints where the tests are done depending on the states reached by the automaton on its runs. Such automata were introduced in studies on semi-structured documents. We do here a detailed comparison between those automata and other models that allow to operate similar tests, like tree automata with constraints between brothers, or tree automata with an auxiliary memory. We show how such automata may be used to verify security properties on cryptographic protocols. Tree automata have already been used to modelize the messages exchanged during a protocol session. By adding equality constraints, we can describe precisely protocol sessions that use a same message several times, hence avoiding an approximation. Then, we answer positively the decision problem of the emptiness of the languages recognized by tree automata with global constraints. By showing that their expressivity is very close from the one of the automata operating on directed acyclic graphs representations of terms, we infer an emptiness decision procedure in double exponential non-deterministic time. Finally, we study the emptiness decision problem for automata with global constraints where we authorize "key constraints", that intuitively allow that all subtrees of a given type in an input tree are distincts. We give an emptiness decision procedure of non-primitive recursive complexity. Key constraints are classicaly used to represent a unique identifier. We describe a non-primitive recusrive emptiness decision procedure. We show that this procedure is very robust and that it allows to extend the automata with additionnal constraints, like counting constraints or local tests, while preserving decidability.

Concevoir et mettre en oeuvre des méthodes pour la spécification, l'analyse et la vérification de logiciels et de systèmes sont les principaux moteurs des activités de recherche présentées dans ce manuscrit. Dans ce cadre, nos travaux se positionnent dans la catégorie dite des méthodes formelles appartenant à la communauté plus large du génie logiciel. A l'interface des travaux théoriques et applicatifs, notre objectif est de contribuer aux méthodes permettant d'assurer la correction et la sûreté des systèmes (fonctionnalité, sécurité, fiabilité, ...) en développant ou en améliorant des langages de spécification, des techniques et des outils permettant leur analyse formelle. Dans ce but, nous nous sommes attaché dans cette thèse à proposer et à étudier un cadre formel permettant la définition de politiques de sécurité et la vérification de leurs propriétés. A cet effet, nous avons proposé un cadre pour la spécification de politiques de sécurité basé sur une approche modulaire dans laquelle une politique est vue comme la composition d'un modèle de sécurité et d'une configuration. Nous avons investigué les possibilités offertes par de telles spécifications lorsque les modèles sont exprimés au moyen de contraintes du premier ordre et les configurations au moyen de programmes logiques. En particulier, nous avons proposé un algorithme permettant de transformer une politique exprimée dans un modèle donné vers une autre politique équivalente (au sens où elle engendre les mêmes autorisations) exprimée dans un autre modèle. Dans un second temps, nous nous sommes proposé de tenir compte des aspects dynamiques de la configuration d'une politique vue comme un état du système sur lequel la politique est mise en oeuvre et où chaque action est associée à une procédure de modification des états. Nous avons proposé un langage formel simple pour spécifier séparément les systèmes et les politiques de sécurité puis avons donné une sémantique des spécifications exprimées dans ce cadre sous la forme de systèmes de réécriture. Nous nous sommes ensuite attachés à montrer que les systèmes de réécriture obtenus permettent l'étude de propriétés de sécurité. Dans une troisième partie, nous nous sommes focalisé sur les mécanismes permettant la mise en oeuvre de politiques de sécurité dans les réseaux. Dans ce cadre, nous avons proposé une spécification des firewalls et de leurs compositions basée sur les automates d'arbres et les systèmes de réécriture puis avons montré en quoi ces spécifications nous permettent d'analyser de façon automatique les politiques de sécurité sous-jacentes. / Designing and applying formal methods for specifying, analyzing and verifying softwares and systems are the main driving forces behind the work presented in this manuscript. In this context, our activities fall into the category of formal methods belonging to the wider community of software engineering. At the interface between theoretical and applied research, our aim is to contribute to the methods ensuring the correction and the safety of systems (security, reliability, ...) by developing or by improving specification languages, techniques and tools allowing their formal analysis. In this purpose, we became attached in this thesis to propose and to study a formal framework allowing the specification of security policies and the verification of their properties. We first proposed a framework for specifying security policies based on a modular approach in which policies are seen as a composition of security models and configurations. We investigated the possibilities opened by such specifications when models are expressed by means of first order constraints and configurations by means of logical programs. In particular, we proposed an algorithm allowing the transformation of a security policy expressed in a given model towards another equivalent policy expressed in another model. Secondly, we suggested taking into account dynamic aspects of policy configurations which can be seen as states of the system on which the policy is applied and where each action is associated with a procedure of states modification. We proposed a simple formal language to specify separately systems and security policies and then gave a semantics of specifications expressed in this framework under the form of rewriting systems. We then attempted to show that the obtained rewriting systems allow the analysis of security properties. In the third part, we focused on mechanisms enforcing security policies in networks. In this context, we proposed a specification of firewalls and their compositions based on tree automata and rewriting systems and then showed how these specifications allow us to analyze in an automatic way the underlying security policies.

Nous proposons une méthode pour aider les administrateurs des applications XML dans la tâche de faire évoluer des schémas en préservant la cohérence de la base de données sans la modifier.<br />L'utilisateur donne au système ce qu'il souhaite comme nouveau document devant être accepté par le schéma.<br />À partir de ce document, le système construit des schémas candidats, qui d'une part préservent la validité de la base de documents et, d'autre part augmentent la classe de documents acceptée par le schéma.<br />L'approche est implantée par un algorithme appelé GREC. <br />Cet algorithme utilise l'automate d'arbre A qui accepte le langage défini par le schéma pour trouver les informations nécessaires à la modification. <br />Plus précisément, il utilise les expressions régulières des règles de transitions de A pour proposer les candidats.<br />Ainsi, les modifications sont faites sur les graphes qui représentent les automates d'états finis construits à partir des expressions régulières concernées.<br />Les expressions régulières engendrées par GREC représentent des schémas présentés à l'utilisateur afin qu'il choisisse le plus adapté à la sémantique de son application.

Le programme de recherches présenté dans cette synthèse s'inscrit dans la double problématique de l'étude des langages d'arbres et de l'apprentissage automatique à partir de données arborescentes. <br /> À la base de ce travail se trouve la question de l'accès et de la manipulation automatique d'informations au format XML au sein d'un réseau d'applications réparties dans internet. La réalisation de ces applications est toujours du ressort de programmeurs spécialistes d'XML et reste hors de portée de l'utilisateur final. De plus, les développements récents d'internet poursuivent l'objectif d'automatiser les communications entre applications s'échangeant des flux de données XML. Le recours à des techniques d'apprentissage automatique est une réponse possible à cette situation. <br /> Nous considèrons que les informations sont décrites dans un langage XML, et dans la perspective de ce mémoire, embarquées dans des données structurées sous forme arborescente. Les applications sont basées alors sur des opérations élémentaires que sont l'interrogation ou les requêtes dans ces documents arborescents ou encore la transformation de tels documents. <br /> Nous abordons alors la question sous l'angle de la réalisation automatique de programmes d'annotation d'arbres, permettant de dériver des procédures de transformation ou d'exécution de requêtes. Le mémoire décrit les contributions apportées pour la manipulation et l'apprentissage d'ensembles d'arbres d'arité non bornée (comme le sont les arbres XML), et l'annotation par des méthodes de classification supervisée ou d'inférence statistique.

Ce travail s'intéresse à la preuve de propriétés de sûreté sur les programmes. Prouver de telles propriétés revient généralement à démontrer que les configurations critiques ne sont jamais atteintes lors de l'exécution du programme. Pour ces propriétés, nous proposons une technique de vérification semi-automatique qui tente de combiner les avantages du model-checking, interprétation abstraite et preuve interactive. Comme en model-checking, cette technique permet de prouver automatiquement des propriétés de sûreté sur les systèmes finis, ainsi que sur certaines classes de systèmes infinis ayant une présentation finie. En dehors de ces classes et comme en interprétation abstraite, notre technique permet d'approcher le comportement infini d'un système par une sur-approximation sûre. Enfin, lorsque les approximations sont trop grossières, il nous est possible d'intervenir manuellement sur la définition des approximations afin de les raffiner et, si cela est possible, de mener la preuve à son terme. Cette approche est basée sur les systèmes de réécriture qui sont un des outils centraux de la déduction automatique. Nous les utilisons comme formalisme pour représenter les programmes: une configuration de programme est représentée par un terme et les transitions entre configurations par des règles de réécriture. Sur de tels modèles, prouver la sûreté d'un programme revient à faire une analyse d'atteignabilité, c.-à-d. vérifier que les termes représentant les configurations critiques sont inatteignables par réécriture des termes initiaux. L'ensemble des termes atteignables est représenté par un automate d'arbre. La construction de cet automate est effectuée en utilisant un algorithme de complétion spécifique. Pour la définition des approximations, nous avons proposé deux langages spécifiques, l'un calqué sur la structure des automates et l'autre utilisant des équations sur les termes. Ce dernier permet, en particulier, d'estimer la précision des approximations construites par rapport à la réécriture modulo équations. Cette technique a été expérimentée pour la vérification de protocoles cryptographiques ainsi que pour le protoypage rapide d'analyses statiques de programmes Java byte code.

Cette thèse est consacrée à l'étude des décalages, ou encore systèmes dynamiques symboliques, définis sur certains monoïdes finiment présentés, $Z^d$ d'une part et les arbres d'autre part. Le principal résultat concernant les décalages multidimensionnels établit que tout décalage effectif de dimension d est obtenu par facteur et sous-action projective d'un décalage de type fini de dimension d+1. De ce résultat nous déduisons que les décalages S-adiques multidimensionnels donnés par une suite effective de substitutions sont sofiques. Sur les décalages d'arbres nous montrons un théorème de décomposition, qui permet d'écrire une conjugaison entre deux décalages d'arbres quelconques comme une suite finie d'opérations élémentaires, les fusions entrantes et les éclatements entrants. De ce théorème, associé à la commutation des fusions entrantes, nous déduisons la décidabilité du problème de conjugaison entre deux décalages d'arbres de type fini. Nous nous intéressons ensuite à la classe des décalages d'arbres sofiques, qui sont exactement ceux reconnus par des automates d'arbres montants dans lesquels tous les états sont à la fois initiaux et finaux. Nous montrons l'existence d'un unique automate d'arbres déterministe, réduit, irréductible et synchronisé qui reconnaît un décalage d'arbres sofique. Enfin nous montrons que l'appartenance à la sous-classe des décalages d'arbres AFT est décidable