Abstract FR:

L'outil rafael sert de support a l'ensemble de cette these. Nous en presentons tout d'abord le contexte formel, c'est-a-dire le langage (osl) permettant la specification de systemes paralleles asynchrones, sa traduction en termes de reseaux de petri ainsi que la structure particuliere des reseaux de petri a files (reseaux rafaeliens) engendres par cette traduction. A ces reseaux rafaeliens, structures en processus communicants, est attachee une semantique formelle derivee de celle du langage amont. Les proprietes fondamentales d'une specification donnee se verifient grace a l'analyse du comportement et des zones d'invariance de son reseau rafaelien associe. Nous presentons ici un ensemble de reductions de ces reseaux. Nous montrons d'abord comment l'application de certaines reductions connues (fusion de places ou de transitions), adaptees aux reseaux traites, preserve la semantique des reseaux; a chaque reduction, nous associons un ensemble de transformations syntaxiques de programmes appliquees a la specification amont. De cette facon la traduction de la specification transformee engendre le reseau a files reduit et les resultats de l'analyse d'un reseau rafaelien reduit peuvent alors etre exprimes en termes de la specification transformee, laissant ainsi le formalisme des reseaux de petri transparent a l'utilisateur. D'autres reductions originales sont presentees. L'une d'elles permet la fusion de deux ensembles de transitions exprimant deux primitives d'entree-sortie. L'application de cette reduction permet, d'un point de vue tres general, de rendre simultanees deux entree-sorties a priori sequentielles. D'autres reductions reduisent la complexite du calcul des invariants du reseau traite et suggerent en particulier d'interferer directement au niveau de l'algorithme de calcul de ces invariants structurels