Offre de stage : Intégration de la bibliothèque RUKIA au logiciel SPIN

Nous cherchons un stagiaire, voici le texte de l’offre :

Réalisation d’un outil de vérification probabiliste de modèles.
Intégration de la bibliothèque RUKIA au logiciel SPIN

Le logiciel SPIN est un “vérificateur de modèles”. Étant donné une description de système par des états et des transitions, le modèle, SPIN permet de vérifier des propriétés de ce modèle par un parcours exhaustif (voir par exemple http://spinroot.com/spin/whatispin.html ). La bibliothèque RUKIA permet l’exploration aléatoire de graphes en tirant des chemins selon une distribution uniforme (voir http://rukia.lri.fr/en/index.html ).
Un modèle étant un cas particulier de graphe, le sujet de ce stage est d’interfacer SPIN et RUKIA de manière à remplacer le parcours exhaustif du modèle, souvent trop coûteux, par une exploration aléatoire uniforme.

*Promela est le langage de description de modèles de SPIN. On peut y inclure des appels de routines C ou C++.
Ce stage aura lieu dans le groupe RASTA du LRI.
Il sera rémunéré.
Durée du stage : 6 mois
Lieu du stage : PCRI, Bâtiment 650, Université Paris-Sud.
Contacts :
Marie-Claude Gaudel, http://www.lri.fr/~mcg/
Sylvain Peyronnet, http://sylvain.berbiqui.org/