Méthodes d'analyse hiérarchique des réseaux de Petri

The aim of this thesis is to define hierarchical analysis methods for Petri nets (a formalism for modelling distributed system control). First, we study the net transformation consisting in replacing open subnets: an equivalence notion is defined, such that if an open subnet is replaced with an equivalent net. The net obtained is equivalent to the original one; then, we define the reentrant net class, for which the equivalence verification, complex in general, becomes simple. Secondly, the investigation of net composition by merging places gives two results: the preservation of home space property if some conditions of independence wrt the shared places are fulfilled, and the preservation of deadlock-freeness when composing ordered-resource nets (in a sense different form the classical solution). Finally, a new norm concept for proving home space property is defined, with composition operations allowing a modular verification of this property.L'objet de cette thèse est de définir des méthodes d'analyse hiérarchique des réseaux de Petri (un formalisme de modélisation du contrôle des systèmes distribués). Premièrement, nous étudions la transformation de réseaux par remplacement de sous-réseaux ouverts: une notion d'équivalence est définie telle que si on remplace un sous-réseau ouvert par un réseau équivalent on obtient un réseau équivalent au réseau d'origine; puis nous définissons la classe des réseaux réentrants, pour laquelle la vérification de l'équivalence, complexe en général, devient simple. Deuxièmement, l'examen de la composition de réseaux par fusion de places conduit à deux résultats: la conservation d'espace d'accueil dans certaines conditions d'indépendance par rapport aux places partagées, et celle de l'absence d'interblocage lors de la composition des réseaux à ressources ordonnées (dans un sens différent de la solution classique). Enfin, un nouveau concept de norme pour la preuve de la propriété d'espace d'accueil est défini, muni d'opérations de composition permettant une vérification modulaire de cette propriété