Voir la source de Validation formelle de composants d'un noyau système embarqué

{{Sujet ter
| labo = [http://www-verimag.imag.fr/ Verimag]
| titre = Validation formelle de composants d'un noyau système embarqué 
| equipe = [http://www-verimag.imag.fr/Synchron.html Synchrone]
| encadrants = Karine.Altisen@imag.fr,Pascal.Raymond@imag.fr,Christophe.Rippert@imag.fr
}}
[[Catégorie:TER]]

=== Thème général === 

Le but de ce [[TER]] est de valider certains composants d'un noyau de système existant à l'aide d'un outil de vérification formelle. Les composants à vérifier sont écrits dans le langage synchrone à flot de données Lustre. On y abordera des problématiques liées aux méthodes formelles confrontées au développement d'ordonnancement statique et dynamique avec tâches périodiques et sur plates-formes matérielles contraintes.

===  Compétences attendues === 

Le candidat devra avoir de solides bases en mathématiques discrètes, [http://intranet.ensimag.fr/KIOSK/Matieres/3MMTL1/ théorie des langages] et logique.

De bonnes connaissances en programmation bas-niveau (cours d'[[Projet_Architecture|Architecture des ordinateurs]], [[Logiciel de Base]]) et en systèmes d'exploitation ([[Pratique_du_Système|Pratique du système]], [[Systèmes_d'exploitation_et_programmation_concurrente|SEPC]]) sont des plus.

===  Contexte du travail === 

L'équipe [http://www-verimag.imag.fr/Synchron.html Synchrone] du laboratoire [http://www-verimag.imag.fr/ Verimag] travaille sur la spécification et la compilation du langage synchrone Lustre permettant de développer des applications embarquées fiables. Ces applications
sont utilisées dans des domaines critiques tels que l'avionique, le nucléaire, etc. où la moindre erreur logicielle peut avoir des conséquences dramatiques.

Depuis quelques années, la nécessité d'embarquer des éléments de système (couche d'abstraction du matériel, ordonnanceur dynamique, etc.) avec les applications s'est imposée, pour permettre la gestion d'événements particuliers (tâches sporadiques devant être traitées de façon urgente) ou faciliter le portage d'une plate-forme matérielle à une autre. Ce sujet se situe dans la continuité des efforts engagés dans l'équipe pour mettre au point des services systèmes fiables permettant l'exécution d'applications synchrones sur des plates-formes matérielles contraintes.

=== Sujet ===

Le travail attendu se base sur un prototype développé dans le cadre d'un stage précédent et dont les résultats sont détaillés dans ce [http://pablo.rauzy.name/files/verimag.pdf document]. Ce prototype est un petit noyau de système dont un composant, l'ordonnanceur, est écrit dans le langage formel Lustre.

Le but de ce TER est d'exploiter cette particularité en validant formellement des composants tels que l'ordonnanceur. Il se déroulera en plusieurs étapes :

# apprentissage du langage Lustre et des problématiques liées (ordonnancement statique, tâches périodiques, etc.),
# apprentissage d'outils de vérification formelle (model-checker) dédiés au langage Lustre
# compréhension de la base de code existante, notamment du code Lustre
# expression de propriétés de bon fonctionnement de l'ordonnanceur et validation formelle.
# éventuellement, développement Lustre d'autres composants système