Séminaires
Séminaire du 5 Novembre 2010
Lieu
LIP6, barre 26-25, salle 105: comment y aller
Programme
14h00-15h00: F. Peschanski, UPMC/LIP6, "Une Caractérisation Décidable pour un Pi-calcul Graphique"
Abstract: Cette présentation introduit les
Pi-graphes, un paradigme visuel pour la modélisation et la
vérification de systèmes mobiles. Le formalisme est une variante
graphique du Pi-calcul permettant d'exprimer des comportements non-terminants
à l'aide d'itérateurs. La sémantique
opérationnelle des Pi-graphe est caractérisée par des
systèmes de transitions étiquetés simples, ce qui permet
d'appliquer des techniques de vérification standards
(vérification d'équivalence par bisimulation,
vérification de modèle). De plus, nous montrons que la relation
de bisimilarité est décidable pour le langage proposé.
Finalement, nous présentons une traduction des Pi-graphes en
réseaux de Petri colorés et nous discutons de la
problématique de préservation sémantique liée
à cette traduction.
15h00-15h30 : S. Hong, UPMC/LIP6, "Calcul d'un ordre statique et hiérarchique pour les diagrammes de décision à partir d'un P/T Net"
Abstract: Le "Model Checking" est de plus en
plus employé dans l'industrie afin de vérifier des
propriétés liées à la sécurité d'un
système, mais très vite nous faisons face au problème de
l'explosion combinatoire de l'espace d'état. Depuis le succès
des Diagrammes de Décision Binaire (BDD) dans ce domaine, les
diagrammes de décision (DDs) sont utilisés afin de contrer ce
problème. D'autres types de DDs ont été employés
depuis, afin d'améliorer l'encodage d'un espace d'état ; l'une
d'entre elles permet d'employer la hiérarchie (SDD). Propres à
tous les DDs, les performances sont fortement dépendantes de l'ordre
des variables statique qui vont représenter le système, et dans
le cas de la hiérarchie, nous parlons maintenant d’un ordre de
variables statique et hiérarchique.
Dans cette étude, nous allons présenter comment exploiter la hiérarchie en utilisant un ordre de variables statique existant afin d’en créer un hiérarchique. Ensuite nous montrerons expérimentalement l'apport de la hiérarchie par rapport à un ordre non hiérarchique. Enfin, nous vous présenterons une nouvelle heuristique, qui va exploiter la structure d'un P/T Net afin de construire directement un ordre statique et hiérarchique.