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.

Dans les systèmes répartis asynchrones, l'horloge logique et le vecteur d'horloges sont deux outils fondamentaux pour gérer la communication et le partage de données entre les entités constitutives de ces systèmes. L'objectif de cette thèse est d'exploiter ces outils avec une perspective d'implantation. Dans une première partie, nous nous concentrons sur la communication de données et contribuons au domaine de la diffusion uniforme à ordre total. Nous proposons le protocole des trains : des jetons (appelés trains) circulent en parallèle entre les processus participants répartis sur un anneau virtuel. Chaque train est équipé d'une horloge logique utilisée pour retrouver les train(s) perdu(s) en cas de défaillance de processus. Nous prouvons que le protocole des trains est un protocole de diffusion uniforme à ordre total. Puis, nous créons une nouvelle métrique : le rendement en termes de débit. Cette métrique nous permet de montrer que le protocole des trains a un rendement supérieur au meilleur, en termes de débit, des protocoles présentés dans la littérature. Par ailleurs, cette métrique fournit une limite théorique du débit maximum atteignable en implantant un protocole de diffusion donné. Il est ainsi possible d'évaluer la qualité d'une implantation de protocole. Les performances en termes de débit du protocole des trains, notamment pour les messages de petites tailles, en font un candidat remarquable pour le partage de données entre coeurs d'un même processeur. De plus, sa sobriété en termes de surcoût réseau en font un candidat privilégié pour la réplication de données entre serveurs dans le cloud. Une partie de ces travaux a été implantée dans un système de contrôle-commande et de supervision déployé sur plusieurs dizaines de sites industriels. Dans une seconde partie, nous nous concentrons sur le partage de données et contribuons au domaine de la RFID. Nous proposons une mémoire répartie partagée basée sur des étiquettes RFID. Cette mémoire permet de s'affranchir d'un réseau informatique global. Pour ce faire, elle s'appuie sur des vecteurs d'horloges et exploite le réseau formé par les utilisateurs mobiles de l'application répartie. Ainsi, ces derniers peuvent lire le contenu d'étiquettes RFID distantes. Notre mémoire répartie partagée à base de RFID apporte une alternative aux trois architectures à base de RFID disponibles dans la littérature. Notre mémoire répartie partagée a été implantée dans un jeu pervasif qui a été expérimenté par un millier de personnes. / In asynchronous distributed systems, logical clock and vector clocks are two core tools to manage data communication and data sharing between entities of these systems. The goal of this PhD thesis is to exploit these tools with a coding viewpoint. In the first part of this thesis, we focus on data communication and contribute to the total order broadcast domain. We propose trains protocol: Tokens (called trains) rotate in parallel between participating processes distributed on a virtual ring. Each train contains a logical clock to recover lost train(s) in case of process(es) failure. We prove that trains protocol is a uniform and totally ordered broadcast protocol. Afterwards, we create a new metric: the throughput efficiency. With this metric, we are able to prove that, from a throughput point of view, trains protocol performs better than protocols presented in literature. Moreover, this metric gives the maximal theoretical throughput which can be reached when coding a given protocol. Thus, it is possible to evaluate the quality of the coding of a protocol. Thanks to its throughput performances, in particular for small messages, trains protocol is a remarkable candidate for data sharing between the cores of a processor. Moreover, thanks to its temperance concerning network usage, it can be worthwhile for data replication between servers in the cloud. Part of this work was implemented inside a control-command and supervision system deployed among several dozens of industrial sites. In the second part of this thesis, we focus on data sharing and contribute to RFID domain. We propose a distributed shared memory based on RFID tags. Thanks to this memory, we can avoid installing a computerized global network. This is possible because this memory uses vector clocks and relies on the network made by the mobile users of the distributed application. Thus, the users are able to read the contents of remote RFID tags. Our RFID-based distributed shared memory is an alternative to the three RFID-based architectures available in the literature. This distributed shared memory was implemented in a pervasive game tested by one thousand users.