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

De Ensiwiki
Aller à : navigation, rechercher


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

Labo Verimag
Equipe Synchrone
Encadrants Karine.Altisen@imag.fr,Pascal.Raymond@imag.fr,Christophe.Rippert@imag.fr

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, théorie des langages et logique.

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

Contexte du travail

L'équipe Synchrone du laboratoire 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 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 :

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