Vérification statique de programmes répartis

Dans les programmes acteurs ou objets concurrents, et plus generalement dans les logiciels clients/serveurs, certaines requetes ne pourront pas etre traitees par leur cible. Une telle requete est appelee message orphelin, elle peut etre : soit un orphelin de surete (son destinataire ne pourra jamais la traiter), soit un orphelin de vivacite (son destinataire pourrait eventuellement la traiter, mais il n'atteindra pas l'etat necessaire a ce traitement). Dans le cadre de l'equipe Vestale qui m'a accueilli, des systemes de type ont ete concus pour detecter les orphelins de surete pour un calcul de processus modelisant les acteurs. Dans cette these, nous adaptons ces analyses statiques pour detecter certains problemes de communication au sein de vrais langages de programmation. Le premier, ML-ACT, une extension de ML avec des primitives du modele d'acteurs concue au sein de l'equipe Vestale. Le second, ERLANG, est un langage focntionnel concurrent et reparti concu par ERICSSON pour construire des applications de telecommunication. Pour detecter les orphelins, nos systemes sont bases sur un processus d'inference qui calcule le type des differentes entites du programme. Les types qui approximent les acteurs sont inspires des types utilises usuellement pour les enregistrements ou les objets. Les systemes de type sont tres sophistiques, ils contiennent une notion de sous-typage et reposent sur des algorithmes d'inference qui collectent des contraintes a partir du code source, puis les resolvent. Leur correction est demontree en utilisant une semantique operationnelle du modele d'acteurs reposant sur un entrelacement de deux reductions (une sur les expressions fonctionnelles et une sur les acteurs). Le formalisme modelisant les acteurs, appele configuration, est general et commun aux deux langages ( qui ne se distinguent donc que par le calcul fonctionnel). En conclusion, nous faisons un bilan des evolutions des theories et techniques qui ont ete necessaires pour adapter des sytemes construits sur un calcul de processus a des langages de programmation complexes.