Master 2013 2014
psar
Intégration de nouveaux services dans CosyVerif


Site :Trac-Intégration de nouveaux services dans CosyVerif
Lieu :LIP6, UPMC
Encadrant : Fabrice Kordon, Alban Linard et Francis Hulin-Hubard

Description

Introduction

Cosyverif est un environnement open source pour la vérification formelle de logiciels complexes (répartis, temps-réel, etc.) qui est conçu comme une plate-forme d’intégration de composants logiciels hébergés dans une machine virtuelle ou sur une machine physique. Le projet est développé conjointement par trois laboratoires d’Île de France : le LIP6 (UPMC), le LIPN et le LSV (ENS de Cachan).

Basé sur une approche client/serveur, Cosyverif est composé d’une interface utilisateur, Coloane, et du serveur, qui est constitué de la plateforme d’intégration (alligator) interfaçant des outils (programmes de vérification, etc) développés et intégrés par les laboratoires contributeurs. Le projet présenté se situe dans ce cadre.

Vous serez encadrés par les ingénieurs de développement du projet, en association avec un enseignant travaillant au LIP6. Le résultat de votre travail devra respecter des critères de qualité précis en vue de son intégration dans la plateforme Cosyverif dont vous deviendrez ainsi un contributeur.

Travail à effectuer

Nous vous proposons d’intégrer deux nouveaux services dans la plateforme Cosyverif.

Le premier service est un service de placement automatique. Les objets manipulés dans la plateforme sont des graphes. En utilisant l’outil Graphviz, vous écrirez un outil de placement automatique des éléments du graphe.

Le second service est un service d’import/export avec le format standard PNML. Ce format d’échange permettra aux outils intégrés dans la plateforme de participer à un concours international de vérification, le Model Checking Contest.