Vérification statique de programmes répartis

Dans les programmes acteurs ou objets concurrents, et plus généralement dans les logiciels clients/serveurs, certaines requêtes ne pourront pas être traitées par leur cible. Une telle requête est appelée message orphelin, elle peut être : soit un orphelin de sûreté (son destinataire ne pourra jamais la traiter), soit un orphelin de vivacité (son destinataire pourrait éventuellement la traiter, mais il n'atteindra pas l'état nécessaire à ce traitement). Dans le cadre de l'équipe Vestale qui m'a accueilli, des systèmes de type ont été conçus pour détectér les orphelins de sûreté pour un calcul de processus modélisant les acteurs. Dans cette thèse, nous adaptons ces analyses statiques pour détecter certains problèmes de communication au sein de vrais langages de programmation. Le premier, ML-ACT, une extension de ML avec des primitives du modèle d'acteurs conçue au sein de l'équipe Vestale. Le second, ERLANG, est un langage focntionnel concurrent et réparti conçu par ERICSSON pour construire des applications de télécommunication. Pour détecter les orphelins, nos systèmes sont basés sur un processus d'inférence qui calcule le type des différentes entités du programme. Les types qui approximent les acteurs sont inspirés des types utilisés usuellement pour les enregistrements ou les objets. Les systèmes de type sont très sophistiqués, ils contiennent une notion de sous-typage et reposent sur des algorithmes d'inférence qui collectent des contraintes à partir du code source, puis les résolvent. Leur correction est démontrée en utilisant une sémantique opérationnelle du modèle d'acteurs reposant sur un entrelacement de deux réductions (une sur les expressions fonctionnelles et une sur les acteurs). Le formalisme modélisant les acteurs, appelé configuration, est général et commun aux deux langages ( qui ne se distinguent donc que par le calcul fonctionnel). En conclusion, nous faisons un bilan des évolutions des théories et techniques qui ont été nécessaires pour adapter des sytèmes construits sur un calcul de processus à des langages de programmation complexes.TOULOUSE-ENSEEIHT (315552331) / SudocSudocFranceF