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 positionnons dans un contexte d'informatique ambiante dans lequel il arrive que les besoins de l'utilisateur n'aient pas été prévus, notamment en situation exceptionnelle. Dans ce cas, il peut ne pas exister de système préconçu qui réponde exactement à ces besoins. Pour les satisfaire, il faut alors pouvoir composer les systèmes disponibles dans l'environnement, et le système composé doit permettre à l'utilisateur de faire des choix à l'exécution. Ainsi, l'utilisateur a la possibilité d'adapter l'exécution de la composition à son contexte. Cela signifie que la composition intègre des structures de contrôle de l'exécution, destinées à l'utilisateur : la composition est dite flexible. Dans cette thèse, nous proposons de répondre au problème de la composition flexible en contexte d'intelligence ambiante avec un planificateur produisant des plans flexibles. Dans un premier temps, nous proposons une modélisation de la planification flexible. Pour cela, nous définissons les opérateurs de séquence et d'alternative, utilisés pour caractériser les plans flexibles. Nous définissons deux autres opérateurs au moyen de la séquence et de l'alternative : l'entrelacement et l'itération. Nous nous référons à ce cadre théorique pour délimiter la flexibilité traitée par notre planificateur Lambda-Graphplan. L'originalité de Lambda-Graphplan est de produire des itérations en s'appuyant sur une approche par graphe de planification. Nous montrons notamment que Lambda-Graphplan est très performant avec les domaines se prêtant à la construction de structures itératives.

Cette thèse prend pour objet le nouage entre l’autoréflexivité et la mise en forme esthétique dans la poésie de Christophe Tarkos, produite dans les années 1990. Elle met en lumière les rapports entre l’élaboration d’une théorie du langage au sein de cette œuvre poétique et ses visées esthétiques totalisantes. Il s’agit d’identifier les principes générateurs de la théorie et de fournir une analyse de ses fondements qui s’ancrent dans la crise de la représentation moderne commençant dans la deuxième moitié du dix-neuvième siècle. Les motifs de la crise revisités par Tarkos inscrivent sa poésie dans une historicité, et notre thèse tente d’interpréter cette actualisation dans une œuvre qui donne forme au monde et à la mémoire individuelle. L’hypothèse qui chapeaute notre étude est que la théorie du langage favorise l’intelligibilité de l’œuvre totalisante en lui offrant un support réflexif. Notre thèse, qui privilégie une méthode fondée sur l’analyse des textes, se divise en trois parties. La première propose une recension de la réception critique de l’œuvre, dont nous retraçons les grandes lignes d’interprétation, de Christian Prigent à Jean-Michel Espitallier. Tout en plaçant Tarkos dans le champ poétique français, cette étape nous permet de positionner notre recherche par rapport à certains lieux communs de la critique. La deuxième partie vise à étudier la théorie du langage de Tarkos à partir de ses manifestes principaux (Le Signe =, Manifeste chou, Ma langue est poétique et La poésie est une intelligence) qui révèlent plusieurs principes, pouvoirs et limites de la langue et de la poésie. Afin de montrer la spécificité du concept de la « pâte-mot » de Tarkos, nous l’étudions dans un dialogue avec la figure de la « pâte » langagière chez la poète française Danielle Collobert. La troisième partie propose une étude de la volonté et de l’esthétique totalisantes dans l’œuvre de Tarkos, qui cherche à donner forme au réel. En effet, la poésie répond à l’excès du réel par diverses stratégies. Tout en voulant représenter son caractère débordant par une énonciation logorrhéique ou en usant de procédés comme celui de la répétition, elle cherche à le maîtriser dans des formes textuelles stables comme des fragments de prose « carrés » (Carrés, Caisses), dans des listes énumératives (Anachronisme) ou dans des réseaux d’images. La volonté totalisante chez Tarkos semble également prendre origine dans un sentiment d’urgence qui concerne, en dernière instance, une bataille contre la finitude. / This dissertation takes as its object the tie between self-reflexivity and aesthetic form in the poetry of Christophe Tarkos, produced in the 1990s. It highlights the relationship between the development of a theory of language within his poetic oeuvre and aims to illustrate its “totalizing” aesthetics. “Theory” is understood as the combination of reflections, meditations and concepts about language and poetry. This thesis endeavors to identify the generating principles in his poetic oeuvre, which are inscribed within the crisis of representation often seen as originating in the mid- nineteenth century. By revisiting this crisis of representation, Tarkos’s poetry can been seen as being located in a historicity. My thesis attempts to interpret this revisiting process through an analysis of a poetic form that gives shape to the world and to individual memory. My assumption is that the theory of language facilitates the intelligibility of his poetry because it provides a reflexive medium. My thesis, which favors a method based on textual analysis, is divided into three parts. The first provides a review of the critical reception of the work, in which I track major lines of interpretation, ranging from Christian Prigent to Jean-Michel Espitallier. Placing Tarkos within the French poetic field allows me to position my research within the commonplace of criticism. The second part investigates the theory of language in his manifestos (Le Signe =, Manifeste chou, Ma langue est poétique et La poésie est une intelligence) that reveal several principles, powers and limits of language and poetry. In order to demonstrate the specificity of the concept of « pâte- mot » (a dough of words) developed by Tarkos, I compare it to the poet Danielle Collobert’s figurative representation of « dough », as « paste ». The third part offers a study of the will and “totalizing” aesthetic present in the work of Tarkos, which seeks to shape the real. Indeed, poetry answers to the excess of the real by various strategies. While wanting to represent his brimming nature through a language akin to logorrhea or by using methods such as repetition, it also seeks to control it in stable textual forms such as « squared » fragments of prose (Carrés, Caisses), in enumerative lists (Anachronisme) or in networks of figures. Tarkos’s willingness to “totalize” also seems to be rooted in a sense of urgency concerning, ultimately, a battle against finitude.

Le travail présenté dans ce mémoire concerne une démarche de conception appliquée à une gestion modale pour les systèmes à événements discrets (SED). Un mode est une configuration particulière du système où celui-ci exploite un ensemble de composants et doit respecter un ensemble de spécifications. La problématique de la gestion de mode porte principalement sur la conception des modes et sur leurs commutations. Notre objectif est de proposer une démarche de conception complètement définie où les spécifications sont assurément respectées, et où seules les commutations désirées entre modes peuvent se produire. Il est également vérifié que toute commutation dans un mode mène de manière sûre dans un autre mode. Pour réaliser cet objectif, nous utilisons la théorie de contrôle par supervision qui permet de concevoir des modèles sûrs par construction tel que les spécifications utilisées pour la construction soient respectées. La démarche proposée possède plusieurs étapes séparant ainsi les différentes études de conception. La première concerne la formalisation du cahier des charges en modèles automate à états. L'étude suivante concerne le comportement interne où celui-ci doit respecter les spécifications propres aux modes, indépendamment des autres modes. Cette étape valide le comportement de chaque mode, avant d'étudier leurs commutations. La troisième étape étudie le comportement commutatif tel que les spécifications de commutations soient respectées. Cette étape spécifie les commutations désirées, et inversement celles non voulues. L'étape suivante est l'exécution d'une fonction de suivi de trajectoire qui vérifie que toutes les commutations mènent bien dans un autre mode. Dans le cas contraire, la fonction de suivi identifie et caractérise les commutations problématiques afin d'aider le concepteur dans la résolution de ces situations. Enfin, une étape de fusion d'états finalise la démarche afin de fournir un modèle par mode qui représente le comportement de celui-ci. Pour montrer l'applicabilité de la démarche proposée, et sa faculté à être utilisée en milieu industriel, nous l'utilisons sur un exemple de taille importante utilisée dans la littérature.

Ce travail est une étude approfondie de la concurrence dans les extensions non-déterministes des réseaux d'interaction de Lafont (langage graphique qui représente, lui, le calcul fonctionnel). Ces extensions sont de trois sortes : les réseaux multirègles, multiports et multifils, et leurs combinaisons donnent ainsi sept types de réseaux. Un premier travail consiste à déterminer une bonne sémantique pour pouvoir comparer ces extensions. On cherche à définir un sémantique opérationnelle structurelle sur les réseaux en se basant sur des technique connues de réécriture des graphes, plus particulièrement celle de " double-pushout with borrowed contexts ". Nous définissons à partir de cette méthode un système d'étiquetage des transitions donné par des règles de dérivations dans le style des langages de processus qui sont le paradigme principal pour étudier les systèmes de calcul concurrents. Nous définissons de plus une sémantique observationnelle sur les réseaux basée sur une notion paramétrique de barbe, qui permet enfin de donner avec précision une notion de traduction entre systèmes. On considère qu'une extension est plus expressive qu'une autre si tout langage de la seconde peut être traduit dans un langage de la première. Ceci nous permet de classer l'ensemble des extensions de manière hiérarchique en trois groupe selon la possibilité de traduire un système de réseau dans un autre. Du plus fort au plus faible : les réseaux contenant des multiports ; ensuite ceux contenant des multifils; enfin les réseaux multirègles. Ceci nous permet de donner un langage universel pour les réseaux dont l'étude donne un point de vue neuf sur les briques fondamentales de la concurrence.

La thèse s'inscrit dans le domaine de la modélisation et de la validation des systèmes modernes complexes. Les systèmes actuels sont en fait d'une complexité sans cesse croissante et formés de plus en plus de composants de natures différentes. Ceci rend leur processus de conception et de validation coûteux et difficile. Il semble être la simple façon permettant de faire face à cette hétérogénéité et à cette complexité est l'approche orientée composant. Suivant cette approche, le système est une entité formée par un ensemble des composants interconnectés. Les composants définissent une interface qui permet d'abstraire leur modèle interne (boîte noire), ce qui favorise la modularité et la réutilisation des composants. L'interaction entre ces composants se fait conformément à un ensemble des règles pré-établies, permettant ainsi d'avoir une vision globale de comportement du système. La conception ainsi que la validation des systèmes modernes reste alors problématique à cause de la nécessité de prendre en compte l'hétérogénéité des différents composants. Dans ce cadre, dans un premier temps, nous définirons un cadre formel générique dans lequel une large famille de formalismes de description de systèmes à base d'états peut être naturellement capturée. Ainsi, nous allons définir un ensemble de règles de composition permettant de mettre en correspondance les différents composants et ainsi de constituer un modèle global du système à concevoir. Dans un second temps, nous proposerons une approche de test d'intégration qui permet de valider le comportement d'un système complexe sous l'hypothèse que chaque composant est testé et validé. Cette approche vise à générer automatiquement des cas de test en s'appuyant sur un modèle global décrit dans notre framework du système sous test.

Cette thèse porte sur la spécification, la vérification et la validation de systèmes critiques à l'aide de méthodes formelles, en particulier, B événementiel. Nous avons travaillé sur l'utilisation de B événementiel pour étudier des algorithmes de contrôle du platooning, à partir d'une version 1D simplifiée vers une version 2D plus réaliste. L'analyse critique du modèle du platooning en 1D a découvert certaines anomalies. La difficulté d'exprimer les théorèmes de deadlock-freeness dans B événementiel nous a motivé pour développer un outil, le générateur de théorèmes de deadlock-freeness, pour construire automatiquement ces théorèmes. Notre évaluation a confirmé que les preuves mathématiques ne sont pas suffisantes pour vérifier la correction d'une spécification formelle : une spécification formelle doit aussi être validée. Nous pensons que les activités de validation, comme les activités de vérification, doivent être associées à chaque raffinement. Pour ce faire, nous avons besoin de meilleurs outils de validation. Certains outils d'exécution existants échouent pour certains modèles non-déterministes exprimés en B événementiel. Nous avons donc conçu et implanté un nouvel outil d'exécution, JeB, un environnement de simulation en JavaScript pour B événementiel. JeB permet aux utilisateurs d'insérer du code sûr à la main pour fournir des calculs déterministes lorsque la traduction automatique échoue. Pour atteindre cet objectif, nous avons défini des obligations de preuve qui garantissent la correction de simulations par rapport au modèle formel.

Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

Cette thèse présente un algorithme qui élimine les racines carrées et les divi- sions dans des programmes sans boucles, utilisés dans des systèmes embarqués, tout en préservant la sémantique. L'élimination de ces opérations permet d'éviter les erreurs d'arrondis à l'exécution, ces erreurs d'arrondis pouvant entraîner un comportement complètement inattendu de la part du programme. Cette trans- formation respecte les contraintes du code embarqué, en particulier la nécessité pour le programme produit de s'exécuter en mémoire fixe. Cette transformation utilise deux algorithmes fondamentaux développés dans cette thèse. Le premier permet d'éliminer les racines carrées et les divisions des expressions booléennes contenant des comparaisons d'expressions arithmétiques. Le second est un algo- rithme qui résout un problème d'anti-unification particulier, que nous appelons anti-unification contrainte. Cette transformation de programme est définie et prou- vée dans l'assistant de preuves PVS. Elle est aussi implantée comme une stratégie de ce système. L'anti-unification contrainte est aussi utilisée pour étendre la transformation à des programmes contenant des fonctions. Elle permet ainsi d'éliminer les racines carrées et les divisions de spécifications écrites en PVS. La robustesse de cette méthode est mise en valeur par un exemple conséquent: l'élimination des racines carrées et des divisions dans un programme de détection des conflits aériens.

Dans cette thèse nous étudions l'isolation mémoire et les mesures de communications efficaces par passage de message dans le contexte des environnements à mémoire partagée et la programmation orientée-objets. L'état de l'art en la matière se base presque exclusivement sur deux techniques complémentaires dites de propriété des objets (ownership) et d'unicité de références (reference uniqueness) afin d'adresser les problèmes de sécurité dans les programmes concurrents. Il est frappant de constater que la grande majorité des travaux existants emploient des méthodes de vérification statique des programmes, qui requirent soit un effort d'annotations soit l'introduction de fortes contraintes sur la forme et les références vers messages échangés. Notre contribution avec SIAAM est la démonstration d'une solution d'isolation réalisée uniquement à l'exécution et basée sur le modèle de programmation par acteurs. Cette solution purement dynamique ne nécessite ni annotations ni vérification statique des programmes. SIAAM permet la communication sans copie de messages de forme arbitraire. Nous présentons la sémantique formelle de SIAAM ainsi qu'une preuve d'isolation vérifiée avec l'assistant COQ. L'implantation du modèle de programmation pour le langage Java est réalisé dans la machine virtuelle JikesRVM. Enfin nous décrivons un ensemble d'analyses statiques qui réduit automatiquement le cout à l'exécution de notre approche.