Les calculs de processus représentent les systèmes concurrents par des processus qui s'exécutent en parallèle et s'échangent des messages. Les calculs avec passivation dispose d'un opérateur spécial qui permet de stopper un processus en cours d'exécution. Le processus suspendu peut ensuite être modifié ou transmis avant d'être réactivé. La passivation rend possible la modélisation de défaillances et d'opérations de reconfiguration dynamique. Nous nous intéressons aux équivalences comportementales dans ces calculs. Le comportement d'un processus est donné par un système de transitions étiquetées, qui exhibe les interactions d'un processus avec son environnement. Des relations, appelées bisimilarités, permettent ensuite d'identifier les processus qui ont le même comportement en comparant leurs interactions. Les bisimilarités définies jusqu'ici dans les calculs avec passivation restent trop complexes pour être utilisée en pratique. En outre il n'existe pas de bisimilarité correcte et complète dans le cas faible, c'est-à-dire lorsque les actions internes aux processus ne sont pas observables. Nous étudions ces deux problèmes dans cette thèse. Nous montrons d'abord qu'il est possible de définir une bisimilarité simple à manipuler pour un calcul avec passivation mais sans restriction. En revanche, nous donnons des contre-exemples qui laissent penser qu'il n'est pas possible de faire de même dans les calculs avec passivation et restriction. Nous définissons également un nouveau type de système de transitions étiquetées, qui permet de caractériser la congruence barbue dans le cas faible. Nous appliquons notre technique à différents calculs dont le Kell.

La vérification formelle est indispensable pour assurer la fiabilité des applications critiques comme les protocoles de communication et les systèmes répartis. La technique de vérification basée sur les modèles (model-checking) consiste à traduire l'application vers un système de transitions étiquetées (STE), sur lequel les propriétés attendues, exprimées en logique temporelle, sont vérifiées à l'aide d'outils appelés évaluateurs (model-checkers). Cependant, les logiques temporelles "classiques", définies sur un vocabulaire d'actions atomiques, ne sont pas adaptées aux langages de description comme LOTOS, dont les actions contiennent des valeurs typées. Cette thèse définit un formalisme appelé XTL (eXecutable Temporal Language) qui permet d'exprimer des propriétés temporelles portant sur les données du programme à vérifier. XTL est basé sur une extension du mu-calcul modal avec des variables typées. Les valeurs contenues dans le STE, extraites à l'aide d'opérateurs modaux étendus, peuvent être passées en paramètre aux opérateurs de point fixe ou manipulées à l'aide de constructions d'inspiration fonctionnelle comme "let", "if-then-else", "case", etc. Les propriétés portant sur des séquences d'actions du programme sont décrites succinctement au moyen d'expressions régulières. Des méta-opérateurs spéciaux permettent l'évaluation des formules sur un STE et l'expression de propriétés temporelles non-standard par exploration de la relation de transition. La sémantique de XTL est formellement définie et des algorithmes efficaces sont proposés pour évaluer des formules temporelles XTL sur des modèles STEs. Un évaluateur XTL est développé et utilisé avec succès pour la validation d'applications industrielles comme le protocole BRP développé par Philips et la couche liaison du bus série IEEE-1394 ("FireWire").