Séminaires
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: bibliothque du LSV
Programme
10h00-11h00: A. Duret-Lutz, LRDE - Epita, "Spot"
Abstract: 
Spot 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: Plusieurs 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: 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.