Abstract FR:

Cette these concerne la specification et modelisation des systemes concurrentes par des reseaux de petri de haut niveau. Tout d'abord nous proposons une generalisation des m-nets, une algebre de reseaux de petri etiquete de haut niveau par une parametrisation qui permet de prendre en compte le comportement d'environnement dans lequel un m-net est execute. La preservation des proprietes essentielles pour l'extension de l'algebre est montree et une caracterisation d'une relation d'equivalence importante du modele est obtenue par la donnee d'un ensemble de regles de transformation. Comme principale nouveaute nous presentons un operateur de raffinement general et en l'etendant un operateur de recursion generale pour les m-nets. Les operation ne demandent de restrictions ni sur l'entourage des transitions a raffiner, ni sur les reseaux raffinants. Plusieurs proprietes de ces operateurs comme la validite, la commutativite par rapport au depliage des m-nets vers les reseaux de petri de bas niveau et leur raffinement sont prouvees, ainsi que quelques proprietes sur des applications successives et enchainees. Les operateurs habituels de composition de reseau peuvent etre synthetises a partir du raffinement general et l'application de l'operation hierarchique dans la semantique des procedures d'un langage de programmation concurrente est illustree.