Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Revue Africaine de Recherche en Informatique et Mathématiques Appliquées Année : 2011

Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf

Résumé

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.
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.
Fichier principal
Vignette du fichier
Vol.14.pp.185-203.pdf (959.76 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

hal-01299417 , version 1 (07-04-2016)

Identifiants

Citer

M. Sogbohossou, D. Delfieu. Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf. Revue Africaine de Recherche en Informatique et Mathématiques Appliquées, 2011, Volume 14 - 2011 - Special issue CARI'10, pp.185-203. ⟨10.46298/arima.1950⟩. ⟨hal-01299417⟩
100 Consultations
797 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More