Abstract FR:

Les méthodes informelles sont inefficaces dans l'assistance à la programmation concurrente et distribuée et sont actuellement remplacées par des outils automatisés basés sur des méthodes formelles. Dans les programmes acteurs et les logiciels clients/serveurs, certaines requêtes ne peuvent être traitées par leur cible et sont appelées messages orphelins. Dans l'équipe Vestale qui m'a accueilli, plusieurs systèmes de type ont été conçus pour détecter les messages orphelins dans un Calcul d'Acteurs primitifs. Mes travaux consistent à y intégrer une description fonctionnelle et réaliste du traitement d'un message par un acteur. Dans ce but nous définissons le mini-langage [lambda]CAP® et sa sémantique à base de système de transitions. Les acteurs peuvent changer dynamiquement d'interface. La description des différentes exécutions possibles en logique temporelle permet alors de mieux appréhender le fonctionnement d'un programme et de décrire les propriétés des analyses statiques réalisées.