Approche formelle pour le développement de services système dans les systèmes embarqués : du modèle à l'implantation

{{Sujet ter
| labo = Vérimag
| titre = Approche formelle pour le développement de services système dans les systèmes embarqués : du modèle a l'implantation 
| equipe = Synchrone
| encadrants = Karine.Altisen@grenoble-inp.fr,Christophe.Rippert@grenoble-inp.fr
}}
[[Catégorie:TER]]

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

* systèmes critiques embarqués
* systèmes d'exploitation temps-réel
* langages synchrones
* exo-noyaux

=== Compétences attendues ===

Ce sujet nécessite un bon niveau de connaissance dans le domaine
de la programmation système (e.g. programmation concurrente,
développement de code bas-niveau, intégration dans le code
existant écrit en C et assembleur ARM). Vu la difficulté technique
du développement attendu, il s'adresse principalement a des étudiants
ayant déjà participé à des projets de développement système (e.g. cours PSE de 2A Ensimag).

=== Contexte du travail ===

Le développement de systèmes embarqués critiques (par exemple avions,
cartes à puce) nécessite l'utilisation de méthodes de conception
fiables basées sur des modèles formels permettant l'utilisation
d'outils de validations automatiques des programmes.

C'est dans cette optique qu'a été conçu le langage synchrone Lustre,
un langage synchrone a flot de données pour la programmation de
programmes réactifs. Il est dote d'une sémantique formelle ce qui
permet la validation des programmes par des techniques telles que le
''model-checking'' ou l'interprétation abstraite.

Il permet une programmation concurrente parfaitement déterministe
grâce a un calcul statique de l'ordonnancement des taches, et
traditionnellement, les applications développées en Lustre s'exécutent
directement sur la machine nue. 

Cependant, l'évolution récente du domaine plaide en faveur de
l'introduction d'un minimum de services systèmes pour faciliter
l'implantation de fonctions supplémentaires. Par exemple,
l'introduction d'une dose limitée d'ordonnancement dynamique pourra
permettre la gestion de taches urgentes (e.g. interruptions) survenant
de façon imprévisibles et s'exécutant pendant une durée inconnue lors
de la conception du système.

Depuis quelques temps déjà, des travaux visent a introduire de
l'ordonnancement dynamique dans l'implémentation de programme Lustre,
tout en garantissant sa sémantique. Ces travaux, pour beaucoup
théoriques, ont conduit a des expérimentations sur des systèmes
d'exploitation temps-réel généralistes.

=== Sujet ===

Le sujet que nous proposons se positionne comme la suite de ces
travaux, en s'attachant aux spécificités des systèmes embarques.  En
effet, dans un système embarque, les besoins en services système sont
a priori restreints et souvent la limite entre le système
d'exploitation et l'application elle-même est floue. Les noyaux de
système d'exploitation généralistes sont souvent monolithiques, ce qui
ne permet pas la souplesse réclamées par ces spécificités  (en
particulier l'extraction des services système réellement nécessaires
pour une application donnée). De plus, une caractéristique particulière
des systèmes embarques est qu'ils sont en général dédies a une seule
application : un système généraliste conçu pour multiplexer les ressources matérielles entre de nombreuses applications n'est donc pas du tout adapté à ce contexte d'utilisation.

Nous proposons d'utiliser une architecture de système d'exploitation
de type "exo-noyau". Cette architecture se caractérise par la séparation entre un nano-noyau contenant uniquement la couche d'abstraction du matériel et un ensemble de services système développés au niveau applicatif. Ces services système sont conçus de façon modulaire pour permettre de n'inclure
que ceux absolument nécessaire a l'exécution des applications. De plus,
cette architecture permet de minimiser la portion de code qui sera exécute
en mode superviseur, ce qui limite l'impact sur le système global d'une
déficience d'un des services système.

=== Résultats attendus ===

Le sujet consiste mettre en place le cadre permettant le développement de
librairies dédiées de services système et à développer de tels services
préalablement valides formellement. Précisément, cela implique : 

* la programmation en Lustre de pilote de périphériques simples (e.g.
UART, capteurs élémentaires) ainsi que de services système comme par exemple
un ordonnanceur dynamique,

* la validation formelle des programmes,

* leur compilation et intégration dans l'exo-noyau.

La plate-forme Lego Mindstorm NXT nous a déjà permis de mener un
certains nombres d'expérimentations sur le sujet et servira de terrain
d'implémentation pour les travaux réalises. Ceci en deux étapes :

1ère étape : implémentation sur la plate-forme Lego Mindstorm NXT en
utilisant le noyau monolithique existant et en y remplaçant les
services système existants par les services systèmes valides

2ème étape : développement d'un nano-noyau et d'une librairie de
services systèmes valides pour la plate-forme.