Analyse des systèmes mobiles par interprétation abstraite.

A mobile system is a pool of agents that may interact with each other. These interactions dynamically change the system, by controlling both creation and destruction of links between agents. These interactions also control the creation of new agents. The size of a mobile system evolves during its computation. This size may be unbounded. A mobile system may describe telecommunication networks, reconfigurable systems, client-server applications, cryptographic protocols, or biological systems. Several models are available according to the application field and the granularity of the observation level. In this thesis, we propose a unifying framework to discover and prove automatically and statically some properties of mobile systems. We propose a metalanguage to encode the most current models for mobility (the p-calculus, the ambients, the join-calculus, the spi-calculus, the BIO-ambients, and so on). The meta-language provides an operational semantics for each encoded model. In these semantics, each agent is identified with the history of its creation, so that this semantics avoids the use of a-conversion. Then, we use the Abstract Interpretation framework to derive abstract semantics, which are sound, decidable, but approximate. In this thesis, we give three generic semantics that we set according to the expected trade-off between accuracy and efficiency. The first analysis focuses on dynamic properties: it captures relations about the creation histories of the agents of the system. This analysis is precise enough to distinguish recursive instances of each agent, even when there is an unbounded number of instances. Thus, we can prove in the case of a clientsever application that the server always returns data to the right client. The second analysis focuses on concurrency properties: it counts the number of occurrences of agents inside the system. This analysis detects mutual exclusion and it bounds the number of agents. The third analysis mixes concurrency and dynamic properties. It gathers the agents of the system in several computation unit. Then, it abstract the number of occurrence of agent in each computation unit. For instance, we can prove the absence of race in the specification of a shared-memory with dynamic allocation that is written in the pi-calculus.Un système mobile est un ensemble de composants qui peuvent interagir entre eux, tout en modifiant dynamiquement le système lui-même. Ces interactions contrôlent ainsi la création et la destruction des liaisons entre les composants, mais aussi la création dynamique de nouveaux composants au sein du système. La taille d'un tel système varie au cours du temps, elle n'est pas bornée en général. Un système mobile peut représenter des réseaux de télécommunication, des systèmes reconfigurables, des applications client-serveur sur la toile, des protocoles cryptographiques, ou des systèmes biologiques. Plusieurs modèles sont disponibles selon le domaine d'application et la granularité du niveau d'observation. Dans cette thèse, nous proposons un cadre de travail unifiant pour découvrir et prouver statiquement (avant leur exécution) et automatiquement les propriétés des systèmes mobiles. Nous proposons un méta-langage dans lequel nous encodons les modèles les plus couramment utilisés dans la littérature (le p-calcul, le calcul des ambients, le join-calcul, le spi-calcul, les BIO-ambients, etc). Pour chaque modèle encodé, le méta-langage calcule une sémantique enrichie dans laquelle à la fois les composants et les objets qu'ils manipulent (adresses mémoires, noms de canaux, clefs secrètes ou partagées, etc) sont identifiés par l'historique de leur création. Ainsi, nous n'utilisons pas de relation de congruence (ni de renommage), ce qui rend l'analyse plus facile. Le cadre général de l'Interprétation Abstraite nous permet ensuite de dériver des sémantiques abstraites, qui sont décidables, correctes, et approchées. Dans cette thèse, nous donnons trois analyses génériques que nous instancions selon le compromis désiré entre le temps de calcul et la précision de l'analyse. La première analyse se concentre sur les propriétés dynamiques du système. Elle infère des relations entre les historiques des objets qui sont manipulés par les composants du système. Cette analyse distingue les instances récursives d'un même objet, et ce, même lorsque le nombre de ces instances n'est pas borné. à titre d'exemple, cette analyse prouve dans le cas d'une application client-serveur à nombre illimité de clients, que les données de chaque client ne sont pas communiquées aux autres clients. La deuxième analyse se concentre sur des propriétés de concurrence. Cette analyse compte le nombre de composants du système. Elle permet de détecter que certains composants ne peuvent pas interagir, car ils ne coexistent jamais. Elle peut aussi garantir à un système qu'il n'épuisera pas les ressources physiques disponibles. Une troisième analyse mêle concurrence et dynamicité