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

[en]
For the formal verification of the concurrent or communicating dynamic systems modeled with Petri nets, the method of the unfolding is used to cope with the well-known problem of the state explosion. An extension of the method to the non safe time Petri nets is presented. The obtained unfolding is simply a prefix of that from the underlying ordinary Petri net to the time Petri net. For a certain class of time Petri nets, a finite prefix capturing the state space and the timed language ensues from the calculation of a finite set of finite processes with valid timings. The quantitative temporal constraints associated with these processes can serve to validate more effectively the temporal specifications of a hard real-time system.

[fr]
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 : [MATH]Mathematics [math], [INFO]Computer Science [cs], [en] Time Petri nets, non safeness, timed unfolding, finite complete prefix, time processes, hard real-time systems.; [fr] 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.

Statistiques de consultation

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