Asynchronous message passing systems are fast becoming a common means for communication between devices. Two problems existing in message passing programs are difficult to solve. The first problem, intended or otherwise, is message-race where a receive may match with more than one send in the runtime system. This non-determinism often leads to intermittent and unexpected behavior depending on the resolution of the race. Another problem is deadlock, which is a situation in that each member process of the group is waiting for some member process to communicate with it, but no member is attempting to communicate with it. Detecting if message-race and/or deadlocks exist in a message passing program are both NP-complete. The difficulty of solving the two problems also comes from three factors that complicate the semantics: asynchronous communication, synchronous barrier, and buffering settings including infinite buffering (the system can buffer messages) and zero buffering (the system has no internal buffering). To solve the above problems with complicating factors, this research provides a novel predictive analysis that initializes a concrete execution and then predicts the behavior of other executions that arise from the initial execution. This research starts with Satisfiability Modulo Theories (SMT) based model checking that provides precise analysis for the program behavior. Unfortunately, a precise analysis using SMT does not scale to large programs. As such, the SMT based model checking is combined with heuristic search for witnessing program properties. The heuristic search is efficient in identifying how sends may match with receives in the runtime as it only looks for the match relations for sends and receives in a small searching space initially; the space is increased only if the program property is not witnessed, until all possible match relations for sends and receives reflected in message non-determinism are found. This research also gives a static analysis approach that is scalable as it does not need to analyze the full set of program behaviors; rather, the static analysis only uses polynomial-time algorithms to identify all potential deadlocks in a send-receive templates given a set of pre-defined deadlock patterns. Given the predictive analysis consisting of SMT based model checking with heuristic search and static analysis, this research is able to solve the two problems above. The work in this dissertation also demonstrates that the predictive analysis is more efficient than the existing tools for verifying message passing programs.

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.

Dans le cadre de cette thèse, nous nous proposons d'étudier le développement et la validation de systèmes dans un contexte temps réel asynchrone. On a choisi d'utiliser le langage AADL pour ses spécificités issues de l'avionique, domaine proche du spatial, et pour la précision de la description de son modèle d'exécution. Le travail de cette thèse se divise en deux axes principaux : d'une part, on étudie l'utilisation du langage AADL dans le cadre du développement d'un logiciel de vol ; et d'autre part, on présente une version réduite du langage AADL, et la définition formelle de son modèle d'exécution à l'aide du langage TLA+. L'objectif de la première partie est d'envisager l'utilisation d'AADL dans le cadre d'un processus de développement existant dans le domaine du spatial. Dans cette partie, on a cherché à identifier des motifs de conceptions récurrents dans les logiciels de vol. Enfin, on étudie l'expression en AADL des différents éléments de ce processus de développement. La seconde partie comporte la définition d'un mini AADL suffisant pour exprimer la plupart des concepts de parallélisme, de communication et de synchronisation qui caractérisent AADL. La partie formalisation est nécessaire afin de pouvoir vérifier des propriétés dynamiques. En effet, la définition formelle du modèle d'exécution permet de décrire le comportement attendu des modèles AADL. Une fois ce modèle défini, on peut à l'aide d'un vérificateur de modèles (model-checker) animer une modélisation AADL ou aborder la vérification de propriétés dynamiques. Cette étude a par ailleurs été menée dans le cadre de la standardisation du langage AADL.

La vérification formelle des contrôleurs logiques a donné lieu à de nombreux travaux scientifiques cette dernière décennie. Elle permet de démontrer (obtention d'un niveau requis de sûreté de fonctionnement (SdF) des systèmes industriels, et tout particulièrement des systèmes critiques. Nos travaux portent sur la preuve des propriétés relatives à la qualité du service rendu par le système automatisé, que nous nommons des propriétés quantitatives. Par exemple, au lieu de vérifier que plusieurs produits ont effectivement été dosés avant d'enclencher un mélange puis une réaction chimique, il peut être important de prouver que la bonne quantité de ces produits a été dosée. Autre exemple, au lieu de prouver qu'un mobile s'arrête dans une position donnée, il peut être important de prouver que cet arrêt en position s'effectue avec une précision garantie. Ce sont de telles propriétés quantitatives que nous nous sommes attachés à être capables de prouver pour les systèmes à évènement discrets (SED), et plus exactement pour une sous classe des SED : les systèmes logiques. Dans ce mémoire nous explorons l'apport des automates hybrides pour la prise en compte simultanée du caractère discret du contrôleur et continu du processus. A cette fin, nous introduisons un formalisme d'automates hybrides à transitions typées et nous proposons une méthodologie de modélisation basée sur des automates modulaires génériques. La vérification est alors obtenue par le model checker PHAVer. Deux études de cas sont présentées en fin de mémoire.

Dans le domaine de la sûreté de fonctionnement, le diagnostic joue <br />un rôle primordial dans l'amélioration de la disponibilité opérationnel le <br />des équipements. Dans les systèmes industriels, une part importante <br />(jusqu'à 80%) est consacrée à la maintenance, test et diagnostic. Pour <br />des systèmes complexes, la résolution des problèmes liés au diagnostic <br />et d'une manière générale de la supervision nécessite la mise en oeu- <br />vre d'une approche générique. Le diagnostic concerne les deux phases <br />indissociables de détection et de localisation. Dans cette thèse nous <br />proposons une approche dynamique de diagnostic pour les systèmes à <br />événements discrets. L'approche proposée basée sur l'exploitation du <br />temps, est applicable à tout système dont l'évolution dynamique dépend <br />non seulement de l'ordre des événements discrets mais aussi de la durée <br />des tâches associées comme pour les processus de communication ou les <br />processus batch. Dans cette thèse, le diagnostic des fautes est réalisé <br />grâce à l'implémentation d'un modèle basé sur l'utilisation des auto- <br />mates temporisés. L'objectif est de concevoir un observateur pour un <br />système donné, qui permet de détecter et localiser les éventuel les dé- <br />fail lances du procédé. Cet observateur est appelé “diagnoser”. Une <br />défail lance est constatée lorsque le séquencement temporel en sortie est <br />incorrect. Nous présentons donc les différentes étapes de la démarche <br />de diagnostic : la construction du diagnoser, la vérification du modèle <br />ainsi qu'une l'application de la démarche sur un exemple réel avec son <br />extension aux systèmes hybrides.

L'augmentation en taille et en complexité des systèmes réactifs font que leur vérification est de plus en plus difficile à comprendre et à appréhender. Dans cette thèse, une approche est proposée pour spécifier et vérifier compositionnellement certains de ces systèmes.<br /><br />Cette approche est basée sur un principe de décomposition supportant un raffinement compositionnel au niveau des composants et au niveau de leur produit synchronisé~: une méthode est présentée pour vérifier le raffinement d'un système à composants à partir du raffinement de ses composants.<br /><br />Les propriétés LTL sont préservées par le raffinement compositionnel présenté ici. De plus, certaines propriétés -- comme les invariants et les propriétés LTL de sûreté -- peuvent être vérifiées compositionnellement durant la phase de vérification du raffinement.<br /><br />Un outil, nommé SynCo, implante cette approche de vérification compositionnelle. Les différents aspects de ce travail sont illustrés par plusieurs exemples~: un robot industriel, un système d'essuyage et un porte-monnaie électronique.

L'utilisation des méthodes formelles pour la conception de protocoles de télécommunication est désormais reconnue comme la seule approche en mesure de garantir leur bon fonctionnement avant la mise en service. Cependant, la complexité toujours croissante ainsi que les contraintes de fiabilité et de sûreté de plus en plus sévères nécessitent l'extension des formalismes de description et l'amélioration continue des méthodes et des techniques de validation. Cette thèse définit une représentation intermédiaire nommé IF pour la description de protocoles. IF est construit à base d'automates temporisés communicants à échéances. Les échéances permettent la modélisation explicite de l'urgence des actions et sont un moyen très fin pour décrire l'évolution temporelle d'un système. Les automates communiquent soit de manière asynchrone, par files d'attente, soit de manière synchrone par rendez-vous. La sémantique opérationnelle de IF est formellement définie et des techniques de simulation efficaces sont proposées. De plus, ayant une structure statique, IF permet l'application intensive des techniques d'analyse statique, comme par exemple celles issues du domaine de l'optimisation de code. Certains informations calculées de cette manière peuvent améliorer considérablement les performances de la validation automatique. Une plate-forme ouverte de validation a été mise en place autour de IF. Elle intègre un grand nombre d'outils autant académiques que industriels et couvre la plupart des techniques actuellement employées pour la vérification et le test des protocoles. Cette plate-forme a été utilisée avec beaucoup de succès sur des protocoles de communication réels, comme par exemple SSCOP ou STARI.

Dans le cadre de la télécommunication, les entreprises développent des protocoles gérant le transfert de données entre machines. Ces protocoles fonctionnent sur le principe d'envoi de messages entre deux parties par l'intermédiaire de canaux non fiables. Pour s'assurer que tous les messages ont bien été reçus, les techniques employées consistent à réémettre les messages perdus et/ou à attendre un laps de temps déterminé avant de conclure à l'échec de la transmission. De plus, les systèmes sont souvent modélisés en fonction de paramètres. Nous avons travaillé sur un modèle mathématique permettant la vérification de spécifications (comportements attendus des systèmes) pour des protocoles manipulant à la fois des compteurs, des files d'attente ou des horloges, ainsi que des paramètres. Le but de l'analyse est de calculer l'ensemble des comportements possibles du système puis de vérifier qu'aucun d'eux ne viole une spécification attendue. Le problème ici est que cet ensemble est infini. En effet, un comportement est fonction des valeurs prises par les variables du système au cours de l'exécution et certaines sont définies sur un domaine infini. Il faut alors pouvoir représenter ces comportements de façon finie et aussi trouver des méthodes pour calculer en un temps fini un ensemble infini. Plus formellement, nous nous sommes placés dans le cadre de l'analyse automatique des systèmes (model-checking). La représentation choisie pour les modèles à compteurs et horloges paramétrés est une extension des matrices de bornes pour laquelle nous avons une méthode exacte d'accélération (calcul en un temps fini d'ensembles de comportements infinis). Du côté pratique, nous avons implanté ces méthodes dans un outil TReX qui est, à notre connaissance, le seul pouvant manipuler de manière exacte des compteurs, des horloges et des files d'attente. Nous avons pu vérifier des exemples conséquents tels que le protocole de retransmission bornée.

As we dive into the digital era, there is growing concern about the amount of personal digital information that is being gathered about us. Websites often track people's browsing behavior, health care insurers gather medical data, and many smartphones and navigation systems store or trans- mit information that makes it possible to track the physical location of their users at any time. Hence, anonymity, and privacy in general, are in- creasingly at stake. Anonymity protocols counter this concern by offering anonymous communication over the Internet. To ensure the correctness of such protocols, which are often extremely complex, a rigorous framework is needed in which anonymity properties can be expressed, analyzed, and ulti- mately verified. Formal methods provide a set of mathematical techniques that allow us to rigorously specify and verify anonymity properties. This thesis addresses the foundational aspects of formal methods for applications in security and in particular in anonymity. More concretely, we develop frameworks for the specification of anonymity properties and propose algorithms for their verification. Since in practice anonymity pro- tocols always leak some information, we focus on quantitative properties which capture the amount of information leaked by a protocol. We start our research on anonymity from its very foundations, namely conditional probabilities - these are the key ingredient of most quantitative anonymity properties. In Chapter 2 we present cpCTL, the first temporal logic making it possible to specify conditional probabilities. In addition, we present an algorithm to verify cpCTL formulas in a model-checking fashion. This logic, together with the model-checker, allows us to specify and verify quantitative anonymity properties over complex systems where probabilistic and nondeterministic behavior may coexist. We then turn our attention to more practical grounds: the constructions of algorithms to compute information leakage. More precisely, in Chapter 3 we present polynomial algorithms to compute the (information-theoretic) leakage of several kinds of fully probabilistic protocols (i.e. protocols with- out nondeterministic behavior). The techniques presented in this chapter are the first ones enabling the computation of (information-theoretic) leak- age in interactive protocols. In Chapter 4 we attack a well known problem in distributed anonymity protocols, namely full-information scheduling. To overcome this problem, we propose an alternative definition of schedulers together with several new definitions of anonymity (varying according to the attacker's power), and revise the famous definition of strong-anonymity from the literature. Furthermore, we provide a technique to verify that a distributed protocol satisfies some of the proposed definitions. In Chapter 5 we provide (counterexample-based) techniques to debug complex systems, allowing for the detection of flaws in security protocols. Finally, in Chapter 6 we briefly discuss extensions to the frameworks and techniques proposed in Chapters 3 and 4.

L'introduction des nouvelles technologies de l'information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu'ils supportent. Cet accroissement de la complexité a un impact sur la sécurité des systèmes. En effet, leurs propriétés ne sont plus réductibles aux propriétés de leurs constituants pris isolément mais émergent d'un réseau d'interactions entre ces constituants qui peut être à l'origine de comportements néfastes et difficiles à prévoir. <br />Notre conviction est que le développement sûr de ces systèmes doit combiner des approches pragmatiques orientées " système ", qui tiennent compte du facteur d'échelle réel d'une automatisation pour appréhender le fonctionnement global du système et son architecture, avec des approches plus formelles qui permettent de s'assurer que les propriétés intrinsèques des constituants contribuent efficacement au respect des exigences " système " formulées par les utilisateurs. <br />Le travail présenté dans ce mémoire définit donc une approche méthodologique basée sur le formalisme SysML (System Modeling Language) permettant l'identification, la formalisation et la structuration d'exigences globales relatives à un système, puis leur projection, sous forme de propriétés invariantes, sur une architecture de composants. La vérification des exigences de sécurité, repose alors, d'une part, sur un raffinement prouvé (par theroem proving) des exigences " système " permettant d'établir leur équivalence avec un ensemble de propriétés intrinsèques relatives à chacun des composants, et d'autre part, sur la vérification formelle (par model checking) de ces propriétés intrinsèques.