Nous étudions les méthodes de preuve des propriétés comportementales d'applications Java distribuées dans lesquelles les objets sur des sites différents coopèrent par appels distants de méthodes. La bibliothèque ProActive fournit un moyen simple et efficace pour mettre en oeuvre cette coopération par définition de primitives qui facilitent la programmation distribuée. Nous présentons une méthode pour définir des modèles comportementaux, compositionne- ls, pour ces applications distribuées, en nous restreignant au cas sans création dynamique d'objets actifs. Nous montrons comment prouver que certaines approximations finies du modèle d'un objet actif représentent fidèlement son comportement. L'analyse des propriétés de l'application (recherche d'inter-blocage, preuves de propriétés de sûreté) peut alors être conduite, sur ces modèles finis compositionnels, en utilisant des outils de vérification automatiques basés sur une sémantique comportementale par bisimulation. Ces analyses compositionnelles ne nécessitant pas de construire l'espace d'états global, souffrent moins du problème d'explosion de l'espace d'état que la plupart des approches du model-checking.