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 contribue à l’étude de la fiabilité et de la sécurité-innocuité des systèmes informatisés, modélisés par des systèmes à événements discrets. Les principales contributions concernent la théorie des Systèmes de Contrôle (notés C Systems) et l’approche par Monitoring des modèles.Dans la première partie de la thèse, nous étudions la théorie des Systèmes de Contrôle qui combine et étend de façon significative, les systèmes de réécriture de la théorie des langages et le contrôle supervisé. Un système de contrôle est une structure générique qui contient deux composants : le composant contrôlé et le composant contrôlant qui restreint le comportement du composant contrôlé. Les deux composants sont exprimés en utilisant le même formalisme comme des automates ou des grammaires. Nous considérons différentes classes de systèmes de contrôle basés sur différents formalismes comme, par exemple, les automates, les grammaires, ainsi que leurs versions infinies et concurrentes. Ensuite, une application de cette théorie est présentée. Les systèmes de contrôle basés sur les automates de Büchi sont utilisés pour vérifier par model-checking, des propriétés définissant la correction sur des traces d’exécution spécifiées par une assertion de type nevertrace.Dans la seconde partie de la thèse, nous investiguons l’approche de monitoring des modèles dont la théorie des systèmes de contrôle constitue les fondations formelles. Le principe pivot de cette approche est la «spécification de propriétés comme contrôleur». En d’autres termes, pour un système, les exigences fonctionnelles, d’une part, et des propriétés, d’autre part, sont modélisées et implantées séparément, les propriétés spécifiées contrôlant le comportement issu des exigences fonctionnelles. De cette approche découle ainsi deux techniques alternatives, respectivement nommées monitoring de modèle et génération de modèle. Cette approche peut être utilisée de diverses manières pour améliorer la fiabilité et la sécurité-innocuité de divers types de systèmes. Nous présentons quelques applications qui montrent l’intérêt pratique de cette contribution théorique. Tout d’abord, cette approche aide à prendre en compte les évolutions des spécifications des propriétés. En second lieu, elle fournit une base théorique à la sécurité fonctionnelle, popularisée par la norme IEC 61508. En troisième lieu, l’approche peut être utilisée pour formaliser et vérifier l’application de guides de bonnes pratiques ou des règles de modélisation appliquées par exemple pour des modèles UML.Ces résultats constituent les bases pour des études futures de dispositifs plus perfectionnés, et fournissent une nouvelle voie pour s’assurer de la fiabilité et de la sécurité-innocuité des systèmes / This thesis contributes to the study of reliability and safety of computer and software systems which are modeled as discrete event systems. The major contributions include the theory of Control Systems (C Systems) and the model monitoring approach.In the first part of the thesis, we study the theory of control systems which combines and significantly extends regulated rewriting in formal languages theory and supervisory control. The control system is a generic framework, and contains two components: the controlled component and the controlling component that restricts the behavior of the controlled component. The two components are expressed using the same formalism, e.g., automata or grammars. We consider various classes of control systems based on different formalisms, for example, automaton control systems, grammar control systems, and their infinite versions and concurrent variants. After that, an application of the theory is presented. The Büchi automata based control system is used to model and check correctness properties on execution traces specified by nevertrace claims.In the second part of the thesis, we investigate the model monitoring approach whose theoretical foundation is the theory of control systems. The key principle of the approach is “property specifications as controllers”. In other words, the functional requirements and property specification of a system are separately modeled and implemented, and the latter one controls the behavior of the former one. The model monitoring approach contains two alternative techniques, namely model monitoring and model generating. The approach can be applied in several ways to improve reliability and safety of various classes of systems. We present some typical applications to show its strong power. First, the approach provides better support for the change and evolution of property specifications. Second, it provides the theoretical foundation of safety-related systems in the standard IEC 61508 for ensuring the functional validity. Third, it is used to formalize and check guidelines and consistency rules of UML.These results lay out the foundations for further study of more advanced control mechanisms, and provide a new way for ensuring reliability and safety

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.

La complexité des systèmes conçus actuellement devient de plus en plus importante. En effet,afin de rester compétitives, les entreprises concevant des systèmes cherchent à leur rajouter de plus en plusde fonctionnalités. Cette compétitivité introduit aussi une demande de réactivité lors de la conception desystèmes, pour que le système puisse évoluer lors de sa conception et suivre les demandes du marché.Un des éléments identifiés comme empêchant ou diminuant cette capacité à concevoir de manière flexibledes systèmes complexes concerne les spécifications des systèmes, et en particulier l’utilisation de la languenaturelle pour spécifier les systèmes. Tout d’abord, la langue naturelle est intrinsèquement ambiguë et celarisque donc de créer des non-conformités si client et fournisseur d’un système ne sont pas d’accord sur lesens de sa spécification. De plus, la langue naturelle est difficile à traiter automatiquement, par exemple, onpeut difficilement déterminer avec un programme informatique que deux exigences en langue naturelle secontredisent. Cependant, la langue naturelle reste indispensable dans les spécifications que nous étudions,car elle reste un moyen de communication pratique et très répandu.Nous cherchons à compléter ces exigences en langue naturelle avec des éléments permettant à la fois de lesrendre moins ambiguës et de faciliter les traitements automatiques. Ces éléments peuvent faire partie demodèles (d’architecture par exemple) et permettent de définir le lexique et la syntaxe utilisés dans lesexigences. Nous avons testé les principes proposés sur des spécifications industrielles réelles et développéun prototype logiciel permettant de réaliser des tests sur une spécification dotée de ces éléments de syntaxeet de lexique. / Systems are becoming more and more complex, because to stay competitive, companies whichdesign systems search to add more and more functionalities to them. Additionally, this competition impliesthat the design of systems needs to be reactive, so that the system is able to evolve during its conception andfollow the needs of the market.This capacity to design flexibly complex systems is hindered or even prevented by various variouselements, with one of them being the system specifications. In particular, the use of natural language tospecify systems have several drawbacks. First, natural language is inherently ambiguous and this can leadsto non-conformity if customer and supplier of a system disagree on the meaning of its specification.Additionally, natural language is hard to process automatically : for example, it is hard to determine, usingonly a computer program, that two natural language requirements contradict each other. However, naturallanguage is currently unavoidable in the specifications we studied, because it remains very practical, and itis the most common way to communicate.We aim to complete these natural language requirements with elements which allow to make them lessambiguous and facilitate automatic processing. These elements can be parts of models (architectural modelsfor example) and allow to define the vocabulary and the syntax of the requirements. We experimented theproposed principles on real industrial specifications and we developped a software prototype allowing totest a specification enhanced with these vocabulary and syntax elements.

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.