Sujet :
Dépliage de réseaux de Petri généraux.
Responsable : Jean-Michel Couvreur et Pascal Weil
Téléphone : 05 40 00 69 34 & 05 40 00 69 28
e-mail : couvreur@labri.fr et weil@labri.fr
Présentation du sujet :
Une des causes principales du problème de l'explosion combinatoire de
la vérification de systèmes est la représentation de la concurrence par entrelacement. Des méthodes (ensembles persistants) évitent
d'explorer l'ensemble de l'espace d'états lors de la vérification en
opérant des réductions basées sur la sémantique de l'ordre partiel du
système tout en préservant certaines propriétés de l'entrelacement. Une
autre approche consiste à réaliser la vérification directement sur une
représentation explicite de l'ordre partiel. Les processus arborescents
(ou dépliages) proposent une sémantique arborescente de l'ordre partiel
pour les réseaux de Petri. McMillan a montré comment les processus
arborescents peuvent être efficacement employés pour la détection des
inter-blocages et le problème de l'accessibilité dans le cas des
réseaux de Petri dont l'espace d'états est fini. Il a décrit la
construction d'un processus arborescent fini contenant l'ensemble des
états accessibles. Récemment, nous avons généralisé cette technique aux
réseaux Petri généraux.
L'objectif du projet est d'implémenter cette
nouvelle technique et d'en évaluer l'efficacité.
Mot-clés : Model-checking, dépliages, réseaux de Petri.
Références :
Commentaires éventuels :