Abstract FR:

Cette these traite de la semantique et la validation des programmes d'acteurs a l'aide des reseaux de petri colores. Dans une premiere etape, nous exposons un algorithme de derivation d'un reseau de petri colore (cpn) a partir d'un programme d'acteurs. L'execution du programme d'acteurs correspond au jeu des jetons dans le cpn correspondant. Les aspects dynamiques de la creation des acteurs et la modification de la topologie d'interaction entre acteurs sont pris en compte par l'evolution des jetons. Nous donnons une semantique du programme d'acteurs a l'aide du graphe des marquages de cpn. Nous prouvons l'equivalence de cette semantique avec celle de g. Agha definie par un systeme de transitions. Nous appliquons l'algorithme de derivation a la translation d'un systeme dynamique a un systeme statique. Dans une deuxieme etape, nous analysons le cpn derive pour etablir des proprietes sur le programme d'acteurs correspondant, par exemple la detection des etats de terminaison et de divergence. L'analyse de cpn se fera a l'aide de deux methodes: celle des marquages equivalents et celle du stubborn set. Nous appliquons ces deux methodes de telle sorte que l'utilisation des reseaux de petri colores devienne superflue. En effet, nous donnons une partition saine et une sous-configuration stubborn qui servent a reduire le systeme de transitions. Nous donnons egalement un ensemble de propositions qui permettent de deduire des proprietes sur le programme d'acteurs a partir du systeme de transitions reduit