RÉSUMÉ.
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.
ABSTRACT.
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.
MOTS-CLÉS : 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.
KEYWORDS : Time Petri nets, non safeness, timed unfolding, finite complete prefix, time processes, hard real-time systems. |
présentation