Lieu : - Équipe Démons du LRI (Université
Paris 11, Orsay) & Projet Coq de l'INRIA, Unité de Rocquencourt, en collaboration avec l'équipe Chir de l'INRIA, Unité de Sophia Antipolis
Information: |
Projet Coq Judicaël Courant- Maître de conférences, Université Paris 11 e-mail: Judicael.Courant@lri.fr |
Équipe ChIR en robotique médicale Ève Coste-Manière - Chargée de recherche e-mail: Eve.Coste-Maniere@sophia.inria.fr |
Description:
Le développement d'outils de robotique complexes en chirurgie soulève le problème de la sécurité des logiciels commandant ces outils. La méthodologie Orccad utilisée décompose le problème d'une part en une partie logique de haut niveau coordonnant les actions élémentaires du robot, d'autre part en des modules algorithmiques commandant ces actions élémentaires. La formalisation de la première partie est relativement bien aboutie, mais les questions de vérification de la partie algorithmique restent très ouvertes. Les objectifs du stage seront les suivants :
- En partant d'un exemple concret développé avec ORCCAD, regarder quelles garanties de sécurité on peut fournir sur un des modules du robot, écrit en C (en fait, un sous-ensemble très restreint de C++). Ces garanties pourront aller de ``toutes les variables du programme sont initialisées'', ``tout au long du programme, les valeurs des variables restent dans tel domaine'' à des garanties impliquant des modèles du comportement de la partie physique du robot.
- Chercher quelles méthodes de validation peuvent être utilisées, adaptées, ou ... restent à inventer pour fournir tout ou partie (selon le temps et la difficulté) de ces garanties. Il serait en particulier intéressant de voir comment les techniques d'interprétation abstraites peuvent s'appliquer, quelles sont leur limites et comment on peut les combiner les techniques de preuves de programmes en théorie des types et plus particulièrement dans l'assistant de preuves Coq.
- Implanter les idées proposées.
Références
- Équipe Chir : www-sop.inria.fr/chir/Theme/SafeProg.html & www-sop.inria.fr/chir/
- Équipe Démons : www.lri.fr/Francais/Recherche/demons/presentation/
- Coq : pauillac.inria.fr/coq/assis-fra.html
- ORCCAD www.inrialpes.fr/iramr/pub/Orccad/orccad-fra.html
- Preuve de Programmes Impératifs : www.lri.fr/~filliatr/publis/these.ps.gz
- Exemple de programmation en ORCCAD : le stage commencera par l'étude d'un des modules du robot présenté en www-sop.inria.fr/chir/personnel/turro/Stanford.html
Retour à la page ChIR