Etude D'accessibilite Des Reseaux De Petri Recursifs Sous Une Semantique De Maximalite

Résumé: Ce travail s'inscrit dans le cadre de la spécification et la vérification des systèmes concurrents à comportement dynamique. Plusieurs études ont montré que le modèle de Réseaux de Petri est le modèle le plus élégant pour décrire le parallélisme, cependant sa limite a été mise en évidence pour la spécification des systèmes dynamiques. Pour cette raison le modèle des Réseaux de Petri Récursifs (RdPRs) a été émergé. Les Réseaux de Petri Récursifs ont été proposés comme un modèle adapté à la manipulation dynamique des objets. En effet, ils se prêtent bien à la spécification et la vérification des systèmes concurrents à structure dynamique. Ils permettent d'une part de modéliser le parallélisme entre les processus du système et d'autre part de simuler la création et la destruction des processus de manière élégante et naturelle (Ceci grâce à une nouvelle transition dite transition abstraite). Dans ce mémoire nous somme intéressé au modèle des Réseaux de Petri Récursifs comme étant un modèle de spécification, pour lequel nous avons proposé une sémantique de vrai parallélisme c'est la sémantique de maximalité. Dans cet objectif nous avons proposé une sémantique opérationnelle de maximalité qui permette d'interpréter tout Réseau de Petri Récursif en un Système de Transitions Etiquetées Maximales (STEM). De ce fait les propriétés relatives au bon fonctionnement d'un système spécifié par un Réseaux de Petri Récursif peuvent être vérifiées sur le système de transitions étiquetées maximales qui lui correspond. En effet la structure de système de transitions étiquetées maximales intègre en elle-même l'information sur l'exécution parallèle des actions. Cette structure nous permet d'exprimer plus facilement les propriétés relatives à l'exécution parallèle des actions. Dans ce travail nous avons proposé un algorithme pour l'étude d'accessibilité pour les réseaux de Petri récursife.

Publié dans la revue: