Résumé : 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 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.Chapitre I Introduction - 1
Chapitre II Non standard semantics for the pi-calculus - 15
Chapitre III Dealing with location - 33
Chapitre IV Meta language - 47
Chapitre V Encoding examples - 71
Chapitre VI Context approximation - 123
Chapitre VII Abstract Interpretation - 157
Chapitre VIII Environment approximation - 169
Chapitre IX Occurrence number approximation - 247
Chapitre X Thread partitioning - 265
Chapitre XI Conclusion - 305