Abstract FR:

Cette these s'interesse a la validation de systemes repartis par analyse de l'espace des etats accessibles. Les symetries presentes dans un systeme, dans son architecture ou dans ses donnees, sont utilisees pour n'explorer qu'une partie des etats accessibles tout en conservant les capacites de verification et de test. L'exploitation des symetries permet alors l'analyse de systemes que l'explosion combinatoire mettait sinon hors de portee des techniques de description formelle. L'idee de base est de reduire le nombre des etats examines en ne considerant qu'un seul representant par classe d'equivalence d'etats symetriques. Grace a des structures syntaxiques introduites dans le langage de specification, le concepteur peut indiquer les symetries d'architecture ou de traitement du systeme considere. Les principales contributions de cette these sont: - les concepts de pool d'agents permutables et de trames de donnees, qui permettent les prises en compte respectives des symetries d'architecture et de donnees, et leur integration dans le langage ccs, - l'interpretation de ces constructeurs sur le domaine des graphes de comportement, au moyen d'une semantique transitionnelle, - la conception d'une algorithmique basee sur les concepts precedents pour la verification par bissimulation et la generation de tests