Titre: Outils logiciels pour le model-checking de structures régulières

Master RSD

Sujet
L'équipe Oasis développe des méthodes et des logiciels pour l'analyse et la vérification des applications construites à base de composants distribués. Un élément important de ces activités est le "model-checker", qui vérifie si une propriété est vraie dans tous les états possibles du comportement de l'application. Nous utilisons aujourd'hui des model-checkers "classiques", basés sur une énumération, explicite ou symbolique, d'un ensemble finis d'états.

Par ailleurs, plusieurs équipes de recherche françaises travaillent au développement de méthodes s'adressant au model-checking sur des espaces d'états infinis mais réguliers (par exemple engendrés par des piles, des files, ou d'autres structures similaires).

Nous chercherons dans ce stage à explorer les possibilités d’utilisation de ces nouvelles méthodes pour notre domaine d'applications.

Encadreur
Eric MADELAINE

Contact
Tel : 04 92 38 78 07
Email : Eric.Madelaine(at)sophia.inria.fr

Laboratoire
Projet Oasis
INRIA Sophia Antipolis

Objectif
Après une étude de l'état actuel des outils de model-checking disponibles, et en particulier de ceux proposés par l'action de recherche PERSEE (langage AltaRica, outils Fast et TRex), le stagiaire étudiera sur des exemples concrets d'applications ProActive les possibilités d'utilisation de ces outils. Il développera une passerelle entre les outils d'analyse de l'équipe et ceux de PERSEE.

Prérequis
Programmation Java et Systèmes distribués, Logique, Gout pour le raisonnement rigoureux

Matériel
Machine et logiciels fourni par Oasis

References
http://www-sop.inria.fr/oasis/Proactive,
http://www.labri.fr/perso/herbrete/persee/

Adresse
Projet OASIS, INRIA, 2004 rte des Lucioles, BP92, 06903 SOPHIA ANTIPOLIS Cedex FRANCE