Abstract FR:

Nous definissons dans cette these la concordance de comportement de deux reseaux de petri, vis-a-vis d'ensembles distingues de leurs places et de leurs transitions mis en correspondance. La concordance de comportement consiste a faire fonctionner ensemble les deux reseaux en les fusionnant selon les places et les transitions associees et a verifier qu'ils ne se perturbent pas l'un l'autre. L'ordre d'association des transitions, dans les sequences engendrees de chaque reseau, est ainsi respecte. Cette etude est directement applicable a la validation des protocoles. Le service fourni par un protocole est defini par l'enchainement des primitives de communication. Nous proposons une methode de validation basee sur une modelisation explicite du protocole et du service attendu, et examinons l'adequation des sequences de primitives de communication en verifiant la non-perturbance des deux modeles. Cette verification est entierement automatisee et l'outil que nous avons developpe donne directement les erreurs de conception du protocole. La methode est appliquee a deux exemples: l'un concerne une version du protocole d, cas monotrame. Cet exemple montre toute l'importance de la modelisation dans les phases preliminaires de propositions de normes. Le deuxieme exemple est un protocole de connexion-deconnexion qui donne une idee de l'extension de notre etude aux reseaux colores