Master 2013 2014
Stages de la spécialité SAR
Développement d’un module IPython pour Spot


Site :LRDE
Lieu :Laboratoire de Recherche et Developpement de l'Épita (LRDE)
Encadrant : Alexandre Duret-Lutz (LRDE/EPITA)
Dates :flexibles
Rémunération :800€ bruts par mois
Mots-clés : Parcours SAR autre qu’ATIAM, professionnel, Parcours SAR, aussi pour STL

Description

IPython (http://ipython.org/) est une architecture de calcul interactif basée sur python, offrant de nombreuses interfaces, dont un "notebook" web permettant de faire des calculs et de les visualiser tout en gardant la trace des différentes étapes. Le mieux, pour avoir une idée des possibilités offertes par IPython, est de suivre une vidéo telle que http://www.youtube.com/watch?v=26wg...

La bibliothèque Spot (http://spot.lip6.fr/) et une bibliothèque C++ d’algorithmes pour construire des model checkers. Elle fournit notamment de nombreux algorithmes pour traduire des formules de logique en automates, ainsi que pour simplifier ces formules et ces automates. Tous ces algorithmes sont accessibles aux programmeurs C++, et les plus importants sont aussi accessibles en ligne de commande sous la forme de commandes Unix. Ces dernières sont documentées ici : http://spot.lip6.fr/userdoc/tools.html

L’objectif du stage est de réaliser une interface entre Spot et Python de façon à pouvoir exécuter des algorithmes de Spot depuis Python, et en particulier depuis le notebook de IPython (où l’interface permettra d’afficher les automates sur lesquels on travaille). Dans un premier temps, on voudrait au moins avoir accès depuis Python à toutes les fonctionnalités actuellement accessibles via les outils en ligne de commandes de Spot. D’autres fonctionnalités de la bibliothèque, pas encore accessible via des outils, seront plus faciles à utiliser depuis python que depuis une ligne de commandes.

Au terme de ce stage, on aimerait que la combinaison ipython+Spot puisse être utilisée pour de l’enseignement (manipulation de formules logique et d’automates) aussi bien que pour de la recherche (exploration interactive à l’aide du notebook).

Ce stage s’adresse à des candidats qui
- sont à l’aise en C++ et en développement sous Unix (la maîtrise d’emacs, de python, et de git sont des plus)
- se soucient d’écrire du code propre et utile (Spot est une bibliothèque open-source utilisée dans d’autres projets)
- n’ont pas peur de se familiariser avec l’univers des automates de Büchi et des formules de logique temporelle. Maîtriser le sujet n’est pas nécessaire pour réaliser l’interface, mais il est quand même nécessaire de ne pas y être allergique !

Bibliographie

http://ipython.org/

http://spot.lip6.fr/

http://spot.lip6.fr/userdoc/tools.html