Séminaire du 23 Mars 2012

Lieu

ENS de Cachan: comment y aller

Attention: le format de ce séminaire est d'une journée complète:

  • Matin: salle des conférences, Pavillon des Jardins
  • Après-midi: bibliothque du LSV

Programme

10h00-11h00: A. Duret-Lutz, LRDE - Epita, "Spot"

Abstract: transparentsSpot est une bibliothèque écrite en C++ offrant des algorithmes et des structures de données pour construire un model checker explicite pour LTL. Après une présentation de l'architecture et des fonctionnalités offertes, nous montrerons comment l'utiliser pour construire un model checker simple, puis comment nous l'utilisons pour expérimenter des approches moins standard.

11h00-11h30: M. Colange, LIP6 - UPMC, "Crocodile, un outil d'analyse symbolique-symbolique pour les Symmetric Nets with Bags"

Abstract: transparentsPlusieurs techniques existent pour lutter contre l'explosion combinatoire des espaces d'états dans le cadre du model checking. Crocodile est un outil de génération d'espace d'états combinant la réduction sous symétries et l'utilisation de diagrammes de décisions. Après la description des mécanismes coupler efficacement les deux approches, nous verrons comment leur utilisation conjointe suggèrent de nouveaux outils de modélisation, notamment la manipulation de bags (multi-ensembles) dans le formalisme des Symmetric Nets.

11h30-12h00 : H. Djafri, LSV - ENS de Cachan, "COSMOS : un outil de model-checking statistique"

Abstract:transparents Dans cet exposé, nous décrirons les fonctionnalités de COSMOS, un outil de model-checking statistique. Les modèles d'entrée sont des réseaux de Petri stochastiques à lois générales avec résolution de conflit de franchissement probabiliste et/ou par priorité. La logique de description des propriétés, HASL, est basée sur une paire constituée d'un automate hybride et d'une expression incluant des occurrences l'opérateur d'espérance. L'expression s'évalue statistiquement sur les chemins (aléatoires) acceptés par l'automate. L'outil dispose aussi d'une fonctionnalité lui permettant de prendre en compte le calcul de très faibles probabilités (de l'ordre de 10^(-30)). La présentation sera illustrée par son utilisation à travers l'environnement CosyVerif.

12h00-14h00: Déjeuner

14h00-15h30 : Travaux pratiques CosyVerif

Abstract: l'objectif est de proposer quelques travaux pratiques d'utilisation des outils sur la plate-forme de vérification CosyVerif.

15h30-16h00: pause café

16h00-17h00: vie du groupe et discussion des actions autour de Cosyverif