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"

transparentsAbstract: 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"

transparentsAbstract: 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.

15h30-16h00: pause café

16h00-16h30: vie du groupe