LSV Seminar

Date

Tuesday, May 13 2008 at 11:00AM

Place

Salle de Conférence (Pavillon des Jardins)

Speaker

Morgan Magnin (IRCCyN)

A mesure que les réseaux proliféraient et prenaient une place temporelle et fonctionnelle des systèmes. Il convient ainsi de développer des formalismes permettant d'écrire et de valider les interactions entre les activités des processeurs et les réseaux de communication. Les réseaux de Petri temporels (RdPT) sont un de ces formalismes. Ils permettent de modéliser la durée de différentes actions sous la forme d'un intervalle de temps. Ils peuvent par ailleurs -bêtre enrichis afin de repr-Aésenter des tâches susceptibles d'-bêtre suspendues puis relanc-Aées (réseaux de Petri à chronomètres notés SwPN).

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 ne 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-bêt majeur du temps dense r-Aéside dans les abstractions symboliques associées, pratiques à mettre en oeuvre et contenant l'explosion combinatoire des états.

Nous nous proposons de comparer les deux approches que sont le temps dense et le temps discret. Notre étude commence par un approfondissement des liens entre réseaux de Petri, RdPT et SwPN en fonction de leur sémantique en temps dense et en temps discret. Nous en déduisons des résultats de décidabilité importants sur les modèles en temps discret, notamment la décidabilité de l'accessibilité d'état sur les SwPN bornés. Nous proposons ensuite 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 concevons 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. Cette procédure nous permet alors de vérifier des propriétés exprimées dans la logique TCTL sur les SwPN en temps discret. Nous aboutissons à des résultats très encourageants, qui permettent d'analyser finement le comportement de modèles à chronomètres.