MeFoSyLoMaRSS

Méthodes Formelles pour les Systèmes Logiciels et Matériels

11/05/2010
Relatore/i : F. Peschanski (UPMC/LIP6), S. Hong (UPMC/LIP6)
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.

Maggiori dettagli qui …
Fabrice.Kordon (at) nulllip6.fr
Mentions légales
Mappa del sito