LOCALITE DANS LE CALCUL ET APPLICATIONS AUX OBJETS DISTRIBUES

CETTE THESE CONCERNE LE -CALCUL, LE CALCUL PROTOTYPE PAR PASSAGE DE NOMS POUR LES PROCESSUS MOBILES, C.-A-D. LES PROCESSUS DONT LA TOPOLOGIE DE COMMUNICATION CHANGE DYNAMIQUEMENT. AU FIL DES ANS, PLUSIEURS VARIANTES ET/OU SOUS-CALCULS DU -CALCUL FURENT PROPOSES AFIN DE MODELISER DE FACON NATURELLE D'IMPORTANTES CLASSES DE SYSTEMES PARALLELES DISTRIBUES ET D'EN PROUVER DES PROPRIETES. NOUS INTRODUISONS LE -CALCUL LOCAL, L, UNE VARIANTE ASYNCHRONE DU -CALCUL DANS LAQUELLE UN PROCESSUS QUI RECOIT UN NOM NE PEUT L'UTILISER QUE DANS DES ACTIONS D'EMISSION. ON PEUT VOIR L COMME UNE BASE SIMPLE POUR LES LANGAGES PARALLELES ET/OU DISTRIBUES COMME PICT ET JOIN. NOUS ETUDIONS LA THEORIE FONDAMENTALE DE L. L'EQUIVALENCE COMPORTEMENTALE QUE NOUS ADOPTONS POUR CE CALCUL EST LA CONGRUENCE A BARBES. NOUS DONNONS DEUX BISIMILARITES ETIQUETEES QUI CARACTERISENT LA CONGRUENCE A BARBES EN L. LA PREMIERE SE BASE SUR UN CODAGE DE L DANS UN SOUS-CALCUL DANS LEQUEL TOUS LES NOMS EMIS SONT PRIVES. LA SECONDE EST BASEE SUR UN NOUVEAU SYSTEME DE TRANSITIONS ETIQUETEES QUI REVELE CE QUI EST OBSERVABLE EN L. NOS BISIMILARITES FORMENT DES RELATIONS DE CONGRUENCE ET PEUVENT ETRE MISES EN VALEUR PAR DES TECHNIQUES DE PREUVE MODULO (UP-TO). DANS LES PREUVES DE CARACTERISATION, AUCUN CONSTRUCTEUR DE COMPARAISON POUR TESTER L'EGALITE ENTRE NOMS N'EST UTILISE. L'UNE DES MOTIVATIONS PRINCIPALES DE L EST SA RICHE THEORIE ALGEBRIQUE. UN CERTAIN NOMBRE D'APPLICATIONS DE CETTE THEORIE SONT PRESENTEES, Y COMPRIS UN ENCODAGE COMPLETEMENT ADEQUAT DE L POLYADIQUE DANS L MONADIQUE. UNE GRANDE PARTIE DE LA THEORIE DE L SE GENERALISE AU -CALCUL ASYNCHRONE, A, DANS LEQUEL IL N'Y A AUCUNE CONTRAINTE SUR LES NOMS RECUS. DES APPLICATIONS DE CETTE NOUVELLE THEORIE DE A SONT : (I) UN ENCODAGE COMPLETEMENT ADEQUAT DE LA MOBILITE EXTERNE (DES NOMS GLOBAUX SONT COMMUNIQUES) A PARTIR DE LA MOBILITE INTERNE (SEULS LES NOMS PRIVES SONT COMMUNIQUES) ; (II) UN ENCODAGE COMPLETEMENT ADEQUAT D'UNE VARIANTE ASYNCHRONE DU CALCUL FUSION DANS A. ENFIN, NOUS UTILISONS LA THEORIE DE L AFIN D'ETUDIER LA MIGRATION DES OBJETS DANS LE LANGAGE DE PROGRAMMATION DISTRIBUEE A BASE D'OBJETS OBLIQ. NOUS DONNONS UNE SEMANTIQUE PAR TRADUCTION (D'UNE ABSTRACTION APPROPRIEE) D'OBLIQ DANS (UNE EXTENSION APPROPRIEE DE) L. EN OBLIQ, LES OBJETS NE SONT PAS PHYSIQUEMENT DEPLACES DURANT LA MIGRATION, MAIS UN CLONE DE L'OBJET EST CREE SUR LE SITE DESTINATION ET L'OBJET ORIGINAL (ET LOCAL) EST TRANSFORME EN UN ALIAS POUR LE CLONE (DISTANT). NOUS ETUDIONS LA CORRECTION DE CETTE FORME DE MIGRATION ; PLUS PRECISEMENT, NOUS CHERCHONS SI LA MIGRATION D'UN OBJET EST TRANSPARENTE POUR SES CLIENTS. NOUS MONTRONS FORMELLEMENT QUE CELA N'EST PAS LE CAS POUR LA SEMANTIQUE D'ORIGINE. POUR CETTE RAISON, NOUS PROPOSONS UNE SEMANTIQUE CORRIGEE D'OBLIQ ET NOUS DONNONS UNE PREUVE DE LA CORRECTION DE LA MIGRATION DES OBJETS VIS-A-VIS DE CETTE NOUVELLE SEMANTIQUE.PARIS-MINES ParisTech (751062310) / SudocSudocFranceF