Groupe MeFoSyLoMa

Séminaire du 20 décembre 2013

Lieu

Programme (journée spéciale CosyVerif et outils de vérification)

14h00-14h30: Alban Linard, LSV, Inria, "État actuel et futur de la plate-forme CosyVerif"

Abstract: Dans cet exposé, nous présentons l'état actuel de la plateforme CosyVerif, permettant d'intégrer des outils de vérification et de les distribuer sous la forme d'un serveur encapsulé dans une machine virtuelle. Nous présenterons ensuite les évolutions futures de la plate-forme.

14h30-14h50: Francis Hulin-Hubard, LSV, CNRS, "CosyVerif vu comme un cœur de vérification pour services de haut niveau"

Abstract: transparents Clitor pour "Command-Line Interface to alligaTOR" est un nouveau client en ligne de commande permettant d'interagir avec le serveur Alligator de la suite CosyVerif

Simple d'acc�ès intuitif et scriptable, Clitor offre, au travers d'une architecture originale, de nouvelles perspectives aux utilisateurs et développeurs d'outils.

14h50-15h20: Fabrice Kordon, LIP6, UPMC, "CosyVerif en enseignement des réseaux de Petri à l'UPMC"

Abstract: transparents Cet exposé présente brièvement l'utilisation de CosyVerif pour enseigner les réseaux de Petri en Master d'informatique à l'UPMC (spécialité SAR - Systèmes et Applications Répartis). Pour cela, nous avons adapté le modèle de distribution de l'environnement afin de le rendre "user friendly" et permettre, outre un déploiement facile sur un ensemble de machines, une utilisation individuelle par les étudiants à des fins d'entrainement.

15h20-15h50: Benoît Barbot, LSV, ENS de Cachan, "Evolution du language de description de formalismes dans CosyVerif"

Abstract: transparents nous présentons une évolution de FML (Formalism Markup Language), le langage de formalismes utilisé dans CosyVerif. Cette évolution comble les lacunes de la première version de FML: difficulté pour définir modulairement des formalismes, manque d'information syntaxique entraînant une non uniformité dans la syntaxe des modè�les, impossibilité d'enrichir les mod�èles avec les résultats des outils.

Ce nouveau langage devrait simplifier la définition des formalismes dans la plate-forme CosyVerif. Nous pourrons l'utiliser pour aider les développeurs d'outils en leur fournissant des bibliothè�ques de manipulation de modè�les. C'est une brique importante de l'évolution de la plate-forme vers l'intégration d'un client léger (Web) en lieu et place de l'actuelle solution basée sur Eclipe.

Séminaires