Répondre à des requêtes de routage requiert que les entités du réseau, nommées routeurs, aient une connaissance à jour sur la topologie de celui-ci, cette connaissance est appelée table de routage. Le réseau est modélisé par un graphe dans lequel les noeuds représentent les routeurs, et les arêtes les liens de communication entre ceux ci.Cette thèse s’intéresse au calcul des tables de routage dans un modèle distribué.Dans ce modèle, les calculs sont effectués par un ensemble de processus placés sur les noeuds. Chaque processus a pour objectif de calculer la table de routage du noeud sur lequel il se trouve. Pour effectuer ce calcul les processus doivent communiquer entre eux. Dans des réseaux de grande taille, et dans le cadre d’un calcul distribué, le maintien à jour des tables de routage peut être coûteux en terme de communication. L’un des thèmes principaux abordés et celui de la réduction des coûts de communication lors de ce calcul. L’une des solutions apportées consisteà réduire la taille des tables de routage, permettant ainsi de réduire les coûts de communication. Cette stratégie classique dans le modèle centralisé est connue sous le nom de routage compact. Cette thèse présente notamment un algorithme de routage compact distribué permettant de réduire significativement les coûts de communication dans les réseaux tels que le réseau internet, i.e. le réseau des systèmes autonomes ainsi que dans des réseaux sans-échelle. Ce document contient également une étude expérimentale de différents algorithmes de routage compact distribués.Enfin, les problèmes liés à la dynamique du réseau sont également abordés. Plusprécisément le reste de l’étude porte sur un algorithme auto-stabilisant de calcul d’arbre de plus court chemin, ainsi que sur l’impact de la suppression de noeuds ou d’arêtes sur les tables de routage stockées aux routeurs. / In order to respond to routing queries, the entities of the network, nammedrouters, require to have a knowledge concerning the topology of the network, thisknowledge is called routing table. The network is modeled by a graph in whichnodes represent routers and edges represent communication links between nodes.This thesis focuses on routing tables computation in a distributed model. In thismodel, computations are done by a set of process placed on nodes. Every processhas for objective to compute the routing table of the node on which he is placed.To perform this computation, processes have to communicate with each other. Inlarge scale network, in the case of a distributed computation, maintaining routingtables up to date can be costly in terms of communication. This thesis focuses mainlyon the problem of communication cost reduction. One of the solution we proposeis to reduce routing tables size which allow to reduce communication cost. In thecentralised model this strategy is well known under the name of compact routing.This thesis presents in particular a distributed compact routing algorithm that allowsto reduce significantly the communication costs in networks like Internet, i.e. theautonomous systems network and others networks that present scale-free properties.This thesis also contains an experimental study of several distributed compact routingalgorithms. Finally, some problems linked to network dynamicity are addressed.More precisely, the problem of network deconnexion during a shortest path treecomputation with auto-stabilisation guaranties, together with a study of the impactof several edges or nodes deletion on the state of the routing tables.

Cette thèse présente un nouveau modèle temporisé appelé timed-pNets pour la modélisation et la vérification des comportements des systèmes distribués hétérogènes. Un défi essentiel de ces systèmes est de spécifier correctement les contraintes de temps du système, dans la mesure où les nœuds dans les systèmes distribués n'ont pas l'horloge physique commune. Timed-pNets utilise un modèle de temps basé sur des horloges logiques, de manière à ce que les mesures de temps dans ce modèle ne reposent pas sur une horloge physique commune. Les timed-pNets ont une structure hiérarchique en arbre: les feuilles de cet arbre sont des Systèmes de Transition Étiquetés paramétrés temporisés (timed-LTSs), et les autres nœuds sont des dispositifs de synchronisation qui permettent de composer les comportements de leurs sous-réseaux. A chaque nœud d'un timed-pNet peut être associée une spécification temporisée, qui consiste en un ensemble d’horloges logiques et de relations sur ces horloges. Les spécifications temporisées sont utilisées pour spécifier les comportements du système, y compris les communications synchrones et asynchrones. Grâce à la spécification temporisée, les timed-pNets peuvent modéliser des systèmes de manière flexible. Les analyses des limites de temps, de la sûreté et de la latence sont discutées par l'étude des conflits de relations entre les horloges logiques du système. Nous utilisons un scénario d'insertion de voitures dans les systèmes de transport intelligents (ITS) comme un exemple pour illustrer l'utilisation de notre modèle timed-pNets. Finalement, l'outil TimeSquare est utilisé pour effectuer une simulation logique et vérifier la validité de notre modèle. / This thesis presents a novel timed model called timed-pNets for modeling and verifying the communication behaviours of heterogeneous distributed systems. Since the nodes in distributed systems have no common physical clock, it brings the challenges of correctly specifying the system time constraints. Timed-pNets build the time model on top of logical clocks such that the time of this model does not rely on a common physical clock. Timed-pNets are tree style hierarchical structures. Each node is associated with a timed specification which consists of a set of logical clocks and some relations on these clocks. The leaves are represented by timed Parametrized Label Transition Systems (timed-pLTSs). Non-leaf nodes (called timed-pNets nodes) are synchronisation devices that synchronize the behaviours of subnets (these subnets can be leaves or non-leaf nodes). Both timed-pLTSs and timed-pNets nodes can be translated to timed specifications. Timed specifications are designed to specify the system behaviours including synchronous and asynchronous communications. Thanks to the timed specification, timed-pNets are able to model systems in a flexible way. Time bound analysis, safety and latency properties are discussed by investigating the relations conflicts between system logical clocks. We take a simple case of car insertion from the area of Intelligent Transportation Systems (ITS) as an example to demonstrate the use of the timed-pNets model. In the end, the TimeSquare tool is used to perform a logical simulation and check the validity of our model.

Répondre à des requêtes de routage requiert que les entités du réseau, nommées routeurs, aient une connaissance à jour sur la topologie de celui-ci, cette connaissance est appelée table de routage. Le réseau est modélisé par un graphe dans lequel les noeuds représentent les routeurs, et les arêtes les liens de communication entre ceux ci.Cette thèse s'intéresse au calcul des tables de routage dans un modèle distribué.Dans ce modèle, les calculs sont effectués par un ensemble de processus placés sur les noeuds. Chaque processus a pour objectif de calculer la table de routage du noeud sur lequel il se trouve. Pour effectuer ce calcul les processus doivent communiquer entre eux. Dans des réseaux de grande taille, et dans le cadre d'un calcul distribué, le maintien à jour des tables de routage peut être coûteux en terme de communication. L'un des thèmes principaux abordés et celui de la réduction des coûts de communication lors de ce calcul. L'une des solutions apportées consisteà réduire la taille des tables de routage, permettant ainsi de réduire les coûts de communication. Cette stratégie classique dans le modèle centralisé est connue sous le nom de routage compact. Cette thèse présente notamment un algorithme de routage compact distribué permettant de réduire significativement les coûts de communication dans les réseaux tels que le réseau internet, i.e. le réseau des systèmes autonomes ainsi que dans des réseaux sans-échelle. Ce document contient également une étude expérimentale de différents algorithmes de routage compact distribués.Enfin, les problèmes liés à la dynamique du réseau sont également abordés. Plusprécisément le reste de l'étude porte sur un algorithme auto-stabilisant de calcul d'arbre de plus court chemin, ainsi que sur l'impact de la suppression de noeuds ou d'arêtes sur les tables de routage stockées aux routeurs.

L´objectif pour ce travail est de proposer une solution de sécurité pour contrôler des flux d´information, spécifiquement par un mécanisme de contrôle d´accès et de flux. L´objectif vise les applications réparties en utilisant les objets actifs avec des communications asynchrones. Il inclut une politique de sécurité et les mécanismes qui imposeront les règles présentes dans de telles politiques. <br />La confidentialité des données et des flux d´information sécurisés est fournie par une vérification dynamique des communications. Tandis que les flux d´information sont généralement vérifiés statiquement, notre attention est concentrée sur des vérifications dynamiques. Pour la réaliser, le modèle proposé a une politique de contrôle de l´information qui inclut des règles discrétionnaires, et comme ces règles sont dynamiquement exécutables, il est possible de tirer profit des contrôles dynamiques pour effectuer en même temps tous les contrôles obligatoires. Les autres avantages de cette approche font que: les contrôles dynamiques n´exigent pas la modification des compilateurs, ne changent pas le langage de programmation, n´exigent pas des modifications aux codes sources existants, et fournissent une flexibilité au moment d´exécution. Ainsi, les contrôles dynamiques sont bien adaptés pour être inclus dans une couche logiciel de type middleware, qui, d´une façon non-intrusive, fournit et assure des services de sécurité aux applications de niveau supérieur. Le modèle de programmation fondamental est basé sur les objets actifs, les communications asynchrones, et les synchronisations de flux de données.

Les systèmes informatiques sont construits par composition de plusieurs sous-systèmes répartis. La manière dont communiquent ces entités, ou pairs, joue un rôle clé dans la bonne marche du système composé. L'étude détaillée de ces interactions est donc essentielle dans le cadre de la vérification et du développement formel de tels systèmes. Ces interactions se décomposent en deux catégories: la communication synchrone et la communication asynchrone. La communication synchrone admet une transmission instantanée de l'information, le message, entre deux entités. La communication asynchrone, en revanche, prend en compte le découplage de la transmission du message en une opération d'envoi puis de réception avec la possibilité que des événements s'intercalent entre les deux donnant ainsi lieu à des variations de comportement, désirables ou non, des systèmes. Souvent considérée comme une entité monolithique duale du monde synchrone, le monde asynchrone se décline en réalité en de multiples modèles qui peuvent induire sur la communication une grande variété de propriétés qu'il convient de caractériser et comparer. Cette thèse se focalise sur les modèles de communication qui orchestrent l'ordre de délivrance des messages : par exemple les modèles dits FIFO qui assurent que certains messages sont reçus dans l'ordre dans lequel ils ont été émis. Nous considérons des modèles de communication classiques de la littérature ainsi que des variations de ces modèles dont nous explicitons les différences parfois négligées. Dans un premier temps nous proposons une formalisation logique abstraite et homogène des modèles de communication considérés et nous les hiérarchisons en étendant des résultats existants. Nous proposons dans un second temps une approche opérationnelle sous forme d'un outil de vérification de compositions de pairs que nous mécanisons à l'aide du langage de spécification TLA+ et du vérificateur de modèles TLC. Cet outil permet de spécifier des pairs communicants et des propriétés temporelles à vérifier pour les différents modèles de communication de façon modulaire. Pour cela, nous apportons un ensemble de spécifications uniformes et opérationnelles des modèles de communication basé sur la notion d'histoires de messages. Nous identifions et prouvons les conditions de leur conformité aux définitions logiques et validons ainsi la pertinence de notre outil. Dans un troisième temps nous considérons des spécifications concrètes de nos modèles de communication, semblables à nombre de celles présentes dans la littérature. Nous disposons donc d'une hiérarchisation des modèles selon les propriétés d'ordre qu'ils garantissent mais également d'une autre hiérarchisation pour un modèle donné entre sa définition logique abstraite et ses implantations concrètes. Ces deux dimensions correspondent à deux dimensions du raffinement. Nous introduisons graduellement par raffinement la notion de communication asynchrone point à point et prouvons, grâce à la méthode Event-B, tous les liens de raffinement entre les différents modèles de communication et leurs déclinaisons. Nous offrons ainsi une cartographie détaillée des modèles pouvant être utilisée pour en développer de nouveaux ou identifier les modèles les plus adaptés à des besoins donnés. Enfin, nous proposons des pistes d'extension de nos travaux à la communication par diffusion où un message peut être envoyé simultanément à plusieurs destinataires. En particulier, nous montrons les différences induites dans la hiérarchie des modèles et les adaptations à effectuer sur notre outil de vérification pour prendre en compte ce mode de communication / Large computing systems are generally built by connecting several distributed subsystems. The way these entities communicate is crucial to the proper functioning of the overall composed system. An in-depth study of these interactions makes sense in the context of the formal development and verification of such systems. The interactions fall in two categories: synchronous and asynchronous communication. In synchronous communication, the transmission of a piece of information - the message - is instantaneous. Asynchronous communication, on the other hand, splits the transmission in a send operation and a receive operation. This make the interleaving of other events possible and lead to new behaviours that may or may not be desirable. The asynchronous world is often viewed as a monolithic counterpart of the synchronous world. It actually comes in multiple models that provide a wide range of properties that can be studied and compared. This thesis focuses on communication models that order the delivery of messages: for instance, the "FIFO" models ensure that some messages are received in the order of their emission. We consider classic communication models from the literature as well as a few variations. We highlight the differences that are sometimes overlooked. First, we propose an abstract, logical, and homogeneous formalisation of the communication models and we establish a hierarchy that extends existing results. Second, we provide an operational approach with a tool that verifies the compatibility of compositions of peers. We mechanise this tool with the TLA+ specification language and its model checker TLC. The tool is designed in a modular fashion: the commmunicating peers, the temporal compatibility properties, and the communication models are specified independently. We rely on a set of uniform operational specifications of the communication models that are based on the concept of message history. We identify and prove the conditions under which they conform to the logical definitions and thus show the tool is trustworthy. Third, we consider concrete specifications of the communication models that are often found in the literature. Thus, the models are classified in terms of ordering properties and according to the level of abstraction of the different specifications. The concept of refinement covers these two aspects. Thus, we model asynchronous point-to-point communication along several levels of refinement and then, with the Event-B method, we establish and prove all the refinements between the communication models and the alternative specifications of each given model. This work results in a detailed map one can use to develop a new model or find the one that best fits given needs. Eventually we explore ways to extend our work to multicast communication that consists in sending messages to several recipients at once. In particular, we highlight the differences in the hierarchy of the models and how we modify our verification tool to handle this communication paradigm.