IOP - Intégration d'Outils de vérification dans la Plate-forme cosyverif

Responsable du projet IOP : Etienne André (LIPN)

CosyVerif [1] (http://cosyverif.org) est une plate-forme d’intégration logicielle développée conjointement par trois laboratoires franciliens : le LIP6, le LIPN et le LSV. L’objectif de CosyVerif est d’intégrer les outils de vérification formelle développés dans ces laboratoires au sein d’un framework commun permettant :

• la mise en valeur des outils et des formalismes associés,
• une meilleure interopérabilité entre outils et formalismes,
• l’équilibrage transparent de la charge lors de la vérification de spécifications complexes.

CosyVerif est composée d’une plate-forme logicielle basée sur des services web : Alligator. Cette dernière peut invoquer localement ou à distance des outils de vérification sous forme de services web. Deux types d’interfaces sont prévues : Coloane, une interface graphique de spécification pour un usage pédagogique et une API php pour un accès programmatique aux outils de CosyVerif.

L’ensemble est diffusé en open source (une affiliation à l’IRILL est en cours d’examen).

CosyVerif est actuellement opérationnelle grâce à l’aide de deux ingénieurs du LSV (dont un à temps partiel) chargés du développement du noyau de la plate-forme et de son architecture logicielle. Ces ingénieurs ont également conçu un processus d’intégration qui a permis à des doctorants ou des collègues d’intégrer quelques outils logiciels. Sur la base de cette procédure type d’intégration, l’objectif de notre projet est d'accroître les possibilités d'intégration, et ainsi d'étoffer le catalogue des outils proposés par CosyVerif.

CosyVerif est actuellement utilisée comme plate-forme d’expérimentation dans les laboratoires impliqués et d’autres laboratoires partenaires. À moyen terme, CosyVerif sera utilisé comme environnement pédagogique pour les enseignements de master. Nous souhaitons également, à travers la définition et la publication de benchmarks types, promouvoir le développement d’outils et la comparaison de techniques de vérification entre elles. À long terme, nous souhaitons promouvoir l’utilisation des techniques de vérification formelle à travers la mise à disposition d’une plate-forme publique accessible publiquement via Internet. Un autre objectif à long terme est la communication entre outils basés sur des formalismes différents et le partage de propriétés d’un modèle par les outils.