Abstract FR:

Dans cette these, nous introduisons une logique modale pour les processus avec passage de valeur permettant d'une part d'exprimer des specifications souples de systemes concurrents et non deterministes pouvant etre satisfaites par une collection d'implementations eventuellement non equivalentes. D'autre part, elle permet la verification compositionnelle de ces systemes. A cause de l'explosion d'etats, l'analyse manuelle de systemes concurrents est tres delicate et sujette aux erreurs. Donc l'aide mecanisee est essentielle. En formalisant notre logique modale dans le systeme d'aide a la preuve pvs, nous fournissons un environnement de preuve interactif permettant aux utilisateurs de specifier leurs systemes et de verifier leur correction en exploitant notre resultat de compositionnalite. L'analyse de systemes concurrents dans notre environnement necessite une forte interaction de l'utilisateur. Pour cela, nous proposons une methodologie de preuve compositionnelle fondee sur notre logique modale. Elle exploite des techniques de decomposition et d'abstraction afin de reduire la preuve interactive d'un systeme a etats infinis a la verification automatique de sa version abstraite a etats finis. Enfin, nous etudions les possibilites d'extension des travaux presentes dans cette these au -calcul, une extension de ccs permettant d'exprimer des processus mobiles.