Master 2013 2014
Stages de la spécialité SAR
Hierarchy of Formalisms in CosyVerif


Site :Hierarchy of Formalisms in CosyVerif
Lieu :LIP6 and/or LSV, ENS Cachan
Encadrant : Lom Messan Hillah Alban Linard
Dates :du 01/04/2014 au 15/09/2014
Rémunération :indemnité de stage standard
Mots-clés : Parcours SAR autre qu’ATIAM, rech./prof., Parcours SAR, aussi pour STL

Description

The goal of this internship is to design and integrate new formalisms in the C osyVerif (http://www.cosyverif.org/) [AHHH+ 13] veri-fication platform.

C osyVerif is a platform dedicated to software veri-fication. It includes tools developed by researchers in formal methods, that belong to several laboratories around Paris. The platform handles several formalisms, such as automata and Petri nets. It allows to specify easily new graph-based formalisms, and to combine existing ones to build more complex formalisms.

C osyVerif currently lacks some usual formalisms, such as temporal logics (CTL, LTL, . . . ). It also lacks several recently published hierarchical and modular formalisms (for instance Modular PNML).

Integrating a new formalism is not a trivial task. In CosyV erif, the formalisms are built using modular pieces, whereas each formalism is usually described as a standalone block in articles. The goal of this internship is to redesign the formalisms found in articles, in order to integrate them in the platform in a modular way.

We are more speci-cally interested in contributions on : • How to transform a formalism to be modular ? • How to refactor an already de-ned formalism hierarchy when needed ? • A comparison with the PNML (http://www.pnml.org/) approach.

Bibliographie

[ABD+ 13] Étienne André, Benoît Barbot, Clément Démoulins, Lom Messan Hillah, Francis Hulin-Hubard, Fabrice Kordon, Alban Linard, and Laure Petrucci. A Modular Approach for Reusing Formalisms in Veri-cation Tools of Concurrent Systems. In ICFEM’13) : 15th International Conference on Formal Engineering Methods, volume to be published of Lecture Notes in Computer Science, page to be published. Springer, October 2013.

[AHHH+ 13] Étienne André, Lom-Messan Hillah, Francis Hulin-Hubard, Fabrice Kordon, Yousra Lembachar, Alban Linard, and Laure Petrucci. CosyVerif : An Open Source Extensi- ble Veri-cation Environment. In Yang Liu and Andrew Martin, editors, ICECCS’13 : 18th IEEE International Conference on Engineering of Complex Computer Systems, pages 33-36. IEEE Computer Society, July 2013.