L'utilisation omniprésente des systèmes informatiques impose de s'assurer de leur bon fonctionnement. Dans ce but, les méthodes de vérification formelle permettent de suppléer les simulations qui ne peuvent être complètement exhaustives du fait de la complexité croissante des systèmes. Le model checking fait partie de ces méthodes et présente l'avantage d'être complètement automatisée. Cette méthode consiste à développer des algorithmes pour vérifier qu'une spécification exprimée la plupart du temps sous la forme d'une formule logique est satisfaite par un modèle du système. Les langages historiques de spécification utilisent comme formules atomiques des variables propositionnelles qui permettent d'exprimer principalement des propriétés portant sur les états de contrôle du modèle. Le but de cette thèse est de vérifier des propriétés plus riches portant sur diverses données manipulées par les modèles: des compteurs, des horloges ou des queues. Ces données peuvent prendre une infinité de valeurs et induisent donc des modèles avec un nombre infini d'états. Nous définissons un cadre général pour l'extension des logiques temporelles avec des contraintes permettant de comparer la valeur des variables a différents états de l'exécution. Nous établissons des résultats de décidabilité et complexité pour des problèmes de model checking impliquant diverses instances de ces extensions. Nous privilégions pour cela l'approche à base d'automates en combinant des constructions connues pour les logiques propositionnelles classiques avec des méthodes d'abstraction des modèles dont les variables sont interprétées dans des domaines infinis.

Cette these contribue a l'etude des semantiques pour la specification et la verification des systemes reactifs. Plus precisement, nous comparons des semantiques comportementales, basees sur la bisimulation avec celles induites par des logiques modales du temps arborescent. Dans la premiere partie, nous considerons les modeles d'entrelacement pour les systemes sequentiels non-deterministes. Plusieurs travaux recents ont montre que dans le cadre des systemes a branchement infini (c-a-d. non-determinisme infini), l'equivalence de bisimulation (forte), reconnue comme l'equivalence semantique de base pour le temps arborescent, est strictement plus fine que celles induites par les logiques du temps arborescent (nous savons depuis longtemps qu'elles coincident sous l'hypothese de branchement fini). Nous utilisons les Processus Ordinaux de Klop, et, en derivant une notion de pouvoir de distinction d'une equivalence semantique, nous montrons dans un cadre parfaitement unifie que la bisimulation est plus fine que les logiques du temps arborescent, mais aussi que pour une large classe de combinateurs, les congruences engendrees par les logiques restent strictement plus faibles que la bisimulation. Dans la deuxieme partie de la these, nous considerons les modeles d'ordre partiel pour les systemes paralleles, dans lesquels on dispose d'une definition satisfaisante de l'operation de raffinement de programme (cette notion est liee a la methode classique de conception hierarchique des programmes). Parmi les equivalences semantiques de la litterature, la history preserving bisimulation est particulierement interessante car c'est une congruence pour l'operation de raffinement quand les systemes n'ont pas d'action invisible. En utilisant une caracterisation de cette equivalence en termes d'une bisimulation avant-arriere, nous exhibons deux caracterisations logiques, ainsi qu'un algorithme de traduction entre ces deux logiques. Nous etudions aussi plusieurs variantes de cette bisimulation avant-arriere. Enfin, nous elargissons le champ de travail en considerant les modeles d'ordre partiel avec actions invisibles. Nous montrons que la bisimulation avant-arriere susmentionnee, adaptee a ce cadre, coincide avec la branching bisimulation sur les arbres causaux, mais aussi avec deux nouvelles equivalences~: l'equivalence de mixed-ordering branching et la history preserving branching bisimulation, que nous etudions.

.

Étude de méthodes de spécification et vérification des protocoles de communication. La méthode de vérification mise en œuvre consiste a évaluer les spécifications du protocole sur un modèle fini qui le représente. Le langage de spécification est basé sur un mu calcul permettant l'expression aussi bien de comportements que de propriétés

Cette thèse se place dans le cadre de la vérification automatique des systèmes distribués. Elle aborde le problème de la spécification pour de tels systèmes, qui consiste à définir un formalisme logique pour décrire des propriétés des comportements de systèmes. On en attend qu'il soit facile d'exprimer les propriétés courantes (accessibilité, sûreté, exclusion mutuelle, vivacité, etc.). On souhaite par ailleurs que la vérification de ces propriétés soient aisée. Il s'agit donc de trouver un compromis entre pouvoir d'expression et simplicité d'utilisation.<br /><br />On s'intéresse ensuite à la modélisation des systèmes concurrents, en recherchant à nouveau un compromis entre réalisme des modèles et facilité de vérification. Les modèles étudiés dans ce travail sont les automates asynchrones, qui modélisent des processus concurrents communiquant par mémoire partagée.<br /><br />La thèse s'intéresse enfin au problème de la synthèse de contrôleur. Étant donné un système spécifié de façon incomplète, donc non-déterministe, en interaction avec un environnement, il s'agit de calculer de manière automatique comment restreindre son comportement afin qu'il vérifie une spécification donnée (quelles que soient les actions de l'environnement). Ce problème se formule en<br />termes de jeux. Dans le cas distribué, les jeux ont naturellement plusieurs joueurs. Dans ce cadre, la plupart des résultats sont négatifs : il est indécidable de savoir si on peut ou non contrôler un tel système. Cette thèse prouve que certaines propriétés de l'architecture de communication garantissent décidabilité pour toute spécification régulière.

Cette thèse porte sur la réalisation d'une maquette du système CESAR, système d'aide à l'analyse d'applications réparties. L'outil réalisé permet de comparer une application décrite par un programme parallèle avec ses spécifications données par un ensemble de formules d'une logique temporelle.

This work studies new algorithms and data structures that are useful in the context of program verification. As computers have become more and more ubiquitous in our modern societies, an increasingly large number of computer-based systems are considered safety-critical. Such systems are characterized by the fact that a failure or a bug (computer error in the computing jargon) could potentially cause large damage, whether in loss of life, environmental damage, or economic damage. For safety-critical systems, the industrial software engineering community increasingly calls for using techniques which provide some formal assurance that a certain piece of software is correct. One of the most successful program verification techniques is model checking, in which programs are typically abstracted by a finite-state machine. After this abstraction step, properties (typically in the form of some temporal logic formula) can be checked against the finite-state abstraction, with the help of automated tools. Alternating automata play an important role in this context, since many temporal logics on words and trees can be efficiently translated into those automata. This property allows for the reduction of model checking to automata-theoretic questions and is called the automata-theoretic approach to model checking. In this work, we provide three novel approaches for the analysis (emptiness checking) of alternating automata over finite and infinite words. First, we build on the successful framework of antichains to devise new algorithms for LTL satisfiability and model checking, using alternating automata. These algorithms combine antichains with reduced ordered binary decision diagrams in order to handle the exponentially large alphabets of the automata generated by the LTL translation. Second, we develop new abstraction and refinement algorithms for alternating automata, which combine the use of antichains with abstract interpretation, in order to handle ever larger instances of alternating automata. Finally, we define a new symbolic data structure, coined lattice-valued binary decision diagrams that is particularly well-suited for the encoding of transition functions of alternating automata over symbolic alphabets. All of these works are supported with empirical evaluations that confirm the practical usefulness of our approaches. / Ce travail traite de l'étude de nouveaux algorithmes et structures de données dont l'usage est destiné à la vérification de programmes. Les ordinateurs sont de plus en plus présents dans notre vie quotidienne et, de plus en plus souvent, ils se voient confiés des tâches de nature critique pour la sécurité. Ces systèmes sont caractérisés par le fait qu'une panne ou un bug (erreur en jargon informatique) peut avoir des effets potentiellement désastreux, que ce soit en pertes humaines, dégâts environnementaux, ou économiques. Pour ces systèmes critiques, les concepteurs de systèmes industriels prônent de plus en plus l'usage de techniques permettant d'obtenir une assurance formelle de correction. Une des techniques de vérification de programmes les plus utilisées est le model checking, avec laquelle les programmes sont typiquement abstraits par une machine a états finis. Après cette phase d'abstraction, des propriétés (typiquement sous la forme d'une formule de logique temporelle) peuvent êtres vérifiées sur l'abstraction à espace d'états fini, à l'aide d'outils de vérification automatisés. Les automates alternants jouent un rôle important dans ce contexte, principalement parce que plusieurs logiques temporelle peuvent êtres traduites efficacement vers ces automates. Cette caractéristique des automates alternants permet de réduire le model checking des logiques temporelles à des questions sur les automates, ce qui est appelé l'approche par automates du model checking. Dans ce travail, nous étudions trois nouvelles approches pour l'analyse (le test du vide) desautomates alternants sur mots finis et infinis. Premièrement, nous appliquons l'approche par antichaînes (utilisée précédemment avec succès pour l'analyse d'automates) pour obtenir de nouveaux algorithmes pour les problèmes de satisfaisabilité et du model checking de la logique temporelle linéaire, via les automates alternants.Ces algorithmes combinent l'approche par antichaînes avec l'usage des ROBDD, dans le but de gérer efficacement la combinatoire induite par la taille exponentielle des alphabets d'automates générés à partir de LTL. Deuxièmement, nous développons de nouveaux algorithmes d'abstraction et raffinement pour les automates alternants, combinant l'usage des antichaînes et de l'interprétation abstraite, dans le but de pouvoir traiter efficacement des automates de grande taille. Enfin, nous définissons une nouvelle structure de données, appelée LVBDD (Lattice-Valued Binary Decision Diagrams), qui permet un encodage efficace des fonctions de transition des automates alternants sur alphabets symboliques. Tous ces travaux ont fait l'objet d'implémentations et ont été validés expérimentalement.

La programmation par aspects est un paradigme de programmation qui permet de mieux séparer les préoccupations d'une application. Un aspect est défini pour chaque préoccupation qui ne peut pas être isolée dans un module. Les aspects sont ensuite ajoutés au programme de base par un processus automatique appelé tissage. Cependant, l'expressivité des langages d'aspect généraux permet de modifier totalement la sémantique du programme de base (par ex., un aspect peut remplacer certains appels de méthode par du code arbitraire). Ce comportement peut entraîner la perte des avantages (lisibilité, maintenabilité, réutilisabilité, etc.) d'une meilleure modularisation des préoccupations. Il devient impossible de raisonner sur le programme de base sans regarder le programme tissé. Cette thèse apporte une réponse aux problèmes ci-dessus en définissant des catégories d'aspects dont l'impact sur la sémantique du programme de base reste sous contrôle. Pour chaque catégorie d'aspects, nous déterminons l'ensemble des propriétés du programme de base qui est préservé par tissage. L'appartenance d'un aspect à une catégorie est garantie par construction grâce à des langages d'aspect dédiés pour chaque catégorie. L'utilisation de ces langages assure que le tissage préservera l'ensemble des propriétés associé à la catégorie concernée. Les propriétés préservées sont représentées comme des sous ensembles de LTL et de CTL*. Nous prouvons formellement que quelque soit le programme de base, le tissage de n'importe quel aspect d'une catégorie préserve les propriétés de la catégorie correspondante. Ces langages et catégories sont définis dans un cadre formel indépendant de tout langage de base ou d'aspect. L'expressivité de ce cadre est montrée en décrivant des primitives complexes de langages d'aspect comme AspectJ et CaesarJ et en effectuant une preuve de correction de transformation d'aspect.

Cette thèse traite du problème de la vérification de systèmes ayant un nombre infini d'états. Ces systèmes peuvent être décrits par plusieurs formalismes tels que des algèbres de processus ou des automates finis munis de structures de données non-bornées (automates à pile, réseaux de Petri ou systèmes à files). Dans une première partie de la thèse nous nous intéressons à la caractérisation de classes de systèmes infinis et de propriétés pour lesquels le problème de vérification est décidable. Nous considérons d'abord la complexité de la vérification du mu-calcul linéaire pour les réseaux de Petri. Ensuite, nous définissons des logiques temporelles qui permettent d'exprimer des propriétés non-régulières comportant des contraintes linéaires sur le nombre d'occurrences d'événements. Ces logiques sont plus expressives que les logiques utilisées dans le domaine. Nous montrons en particulier que le problème de la vérification d'une logique qui est plus expressive que le mu-calcul linéaire est décidable pour des classes de systèmes infinis telles que les automates à pile et les réseaux de Petri. Une deuxième partie de la thèse est consacrée aux systèmes communicant par files d'attente, dont le problème de vérification est en général indécidable. Nous appliquons le principe de l'analyse symbolique à ces systèmes. Nous proposons des structures finies qui permettent de représenter et de manipuler des ensembles infinis de configurations de tels systèmes. Ces structures permettent de calculer l'effet exact d'une exécution répétée de tout circuit dans le graphe de transitions du système. Ainsi, chaque circuit peut être considéré comme une nouvelle "transition" du système. Nous utilisons ce résultat pour accélérer le calcul de l'ensemble des configurations atteignables d'un système afin d'augmenter les chances de terminaison de ce calcul.

Ce travail porte sur la specification et la verification des systemes temps reel. Nous presentons une algebre de processus temporises ATP, qui permet de decrire de tels systemes en utilisant divers operateurs temporels. Sa semantique operationnelle est basee sur l'hypothese de synchronisme des langages synchrones. Elle definit les modeles des processus comme des systemes de transitions etiquetees, dans lesquels l'evolution discrete du temps est denotee par une etiquette particuliere. Une axiomatisation complete offre la possibilite de comparer deux termes de l'algebre modulo l'equivalence forte sans construire leurs modeles. Nous generalisons ensuite la semantique d'ATP a des domaines temporels quelconques, en particulier des domaines denses. Nous montrons qu'une propriete de surete est satisfaite par un processus pour tout domaine temporel discret si elle l'est pour un domaine dense. Nous etudions dans un deuxieme temps les graphes temporises, qui sont des automates etendus par des compteurs de temps. Nous presentons une methode de traduction d'ATP vers les graphes temporises qui preserve la semantique des processus. Le graphe obtenu presente l'interet d'etre de taille independante des valeurs des delais apparaissant dans la description, car les contraintes temporelles y sont exprimees symboliquement. Finalement, nous decrivons un algorithme de verification de proprietes sur les graphes temporises. Il consiste a evaluer symboliquement des formules d'une logique temporelle temps reel en evitant l'explosion combinatoire du nombre d'etats des modeles de bas niveau causee par les valeurs des delais. Nous obtenons ainsi les principes theoriques d'un outil de description et de verification de systemes temps reel.