M. Sogbohossou ; D. Delfieu - Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf

arima:1950 - Revue Africaine de Recherche en Informatique et Mathématiques Appliquées, 16 octobre 2011, Volume 14 - 2011 - Numéro spécial CARI'10 - https://doi.org/10.46298/arima.1950
Dépliage des réseaux de Petri temporels à modèle sous-jacent non saufArticle

Auteurs : M. Sogbohossou 1; D. Delfieu 2

  • 1 Laboratoire d'Electrotechnique, de Télécommunication et d'Informatique Appliquée
  • 2 Institut de Recherche en Communications et en Cybernétique de Nantes

Pour la vérification formelle des systèmes dynamiques concurrents ou coopérants modélisés à l’aide des réseaux de Petri, la méthode du dépliage est utilisée pour endiguer le phénomène bien connu de l’explosion combinatoire. Une extension de la méthode aux réseaux de Petri temporels à modèle sous-jacent non sauf est présentée. Le dépliage obtenu est simplement un préfixe de celui du réseau de Petri ordinaire sous-jacent au réseau temporel. Pour une certaine classe de réseaux temporels, un préfixe fini capturant l’espace d’état et le langage temporisé découle du calcul d’un ensemble fini de processus finis réalisables. Les contraintes temporelles quantitatives associées à ces processus peuvent servir à valider plus efficacement les spécifications temporelles d’un système temps réel dur.


Volume : Volume 14 - 2011 - Numéro spécial CARI'10
Publié le : 16 octobre 2011
Soumis le : 24 mars 2011
Mots-clés : Time Petri nets, non safeness, timed unfolding, finite complete prefix, time processes, hard real-time systems.,Réseaux de Petri temporels,caractère non sauf,dépliage temporel,préfixe complet fini,processus temporisés,systèmes temps réel durs.,[MATH] Mathematics [math],[INFO] Computer Science [cs]

Statistiques de consultation

Cette page a été consultée 217 fois.
Le PDF de cet article a été téléchargé 306 fois.