Accès direct au contenu

ENS Cachan

Version anglaise
Recherche avancée
aide Portail documentaire


Accueil > Actualités > Actualités de la recherche

Diffusion des savoirs, Recherche - Valorisation

À la recherche de méthodes efficaces pour la vérification de réseaux de

le 13 mai 2008
Mardi 13 mai, 11 h

Séminaire de Morgan Magnin (IRCCyN), à l'invitation du Laboratoire spécification et vérification (LSV).

À 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 être enrichis afin de représenter des tâches susceptibles d'être suspendues puis relancé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ê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 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.
Type :
Séminaires - conférences
Contact :
Steve Kremer
Lieu(x) :
Campus de Cachan
Salle de conférence du Pavillon des Jardins

Recherche d'une actualité

Recherche d'une actualité