Réseaux de Petri à chronomètres
Par : Magnin, Morgan
Document archivé le : 02/02/2010
Dans cette thèse, nous comparons les approches en temps dense et en temps discret pour la vérification de systèmes temps réel via une extension des réseaux de Petri temporels, appelée réseaux de Petri à chronomètres. Le temps dense consiste à considérer le temps comme une grandeur dense tandis que le temps discret l'assimile à une grandeur discrète. Les applications physiques évoluent par rapport au temps physique qui est continu ; toutefois, l'évolution du procédé n'est en général observée par le système informatique qui le pilote qu'à des instants particuliers (échantillonnage ou observations sporadiques). De plus, le système de pilotage est composé de tâches qui sont exécutées sur un (ou plusieurs) processeur(s) dont le temps physique est discret. Le recours à un temps dense lors de la modélisation conduit donc à une surapproximation du système informatique. Mais l'intérêt majeur du temps dense réside dans les abstractions symboliques associées, pratiques à mettre en oeuvre et contenant l'explosion combinatoire des états. Nous avons commencé par améliorer les méthodes de calcul de l'espace d'états en temps dense. Nous avons ensuite établi une classification des réseaux de Petri en temps discret. Nous avons proposé une méthode efficace de calcul énumératif de l'espace d'états de modèles en temps discret. Comme toute méthode purement énumérative, celle-ci souffre toutefois de l'explosion combinatoire du nombre d'états. C'est pourquoi nous avons conçu une méthode symbolique permettant de calculer l'espace d'états d'un modèle en temps discret en adaptant les techniques habituellement réservées au temps dense.
IMPORTANT : OBLIGATIONS DE LA PERSONNE CONSULTANT CE DOCUMENT
Conformément au Code de la propriété intellectuelle, nous rappelons que le document est
destiné à un usage strictement personnel. Les "analyses et les courtes citations justifiées
par le caractère critique, polémique, pédagogique, scientifique ou d'information" sont autorisées
sous réserve de mentionner les noms de l'auteur et de la source (article L. 122-4 du Code de la
propriété intellectuelle). Toute autre représentation ou reproduction intégrale ou partielle,
faite sans le consentement de l'auteur ou de ses ayants droit, est illicite.
De ce fait, nous vous rappelons notamment que, sauf accord explicite de l'auteur de la thèse, vous n'êtes pas autorisé à rediffuser ce document sous quelque forme que ce soit (impression papier, transfert par voie électronique, ou autre). Tout contrevenant s'expose aux peines prévues par la loi.
Fichier(s) associé(s) au document :
2007NANT2144_Magnin_these.pdf
2007NANT2144_Magnin_these.pdf