Proposition d’une méthode alpha-réduit pour les réseaux de petri récursifs sous une sémantique de vrai parallélisme

Abstract

Ce travail traite la spécification et la vérification formelles des systèmes concurrents dynamiques. Un modèle de réseau de Petri récursif sous une sémantique basée sur la maximalité est utilisé pour modéliser de tels systèmes. Le but de ce travail est de surmonter le problème de l'explosion combinatoire de graphe d'état. Comme solution, nous proposons un algorithme de génération à la volée d'un système de transitions étiquetées maximales (STEM en abrégé) modulo la relation de a-équivalence. L'intérêt de l'algorithme de réduction de l'espace d'état est mis en évidence en considérant la spécification d'un protocole de couche transport de la classe l'initiative à l'expéditeur. Les propriétés attendues du protocole sont vérifiées en considérant le STEM réduit, en utilisant l'outil développé mettant en oeuvre l'approche proposée.