Développement du noyau logiciel du projet.
Début : M6
Fin : M11
Responsable : CEA
Participants : CEA, INRIA
L'objectif est de développer un noyau fournissant un certain nombre de services élémentaires à travers une interface extensible permettant d'ajouter simplement de nouvelles fonctionnalités. En particulier ce noyau fournira une interface permettant de lire, de stocker et d'analyser des propriétés associées à des points de programme ou à des points d'instances particulières d'un programme, d'analyser un programme C, de parcourir de façon générique ce code C en suivant les constructions syntaxiques du langage ou en suivant le flot de contrôle du programme et de gérer des projets de vérification (sauvegarde, reprise, gestion de versions).
T2.0 : Description de l'architecture du noyau
On définira une architecture extensible à l'aide de greffons logiciels (Plug-Ins) indépendants. De plus il faudra définir comment le noyau stockera les propriétés et comment il garantira la cohérence des informations qu'il conserve.
T2.1 : Spécification fonctionnelle du noyau
En partant de l'analyse de besoins du sous-projet 1, nous préciserons l'ensemble des services nécessaires au noyau. Cet ensemble comportera au moins les services décrits dans les objectifs de ce sous-projet.
T2.2 : Implantation du noyau
Nous implanterons le noyau en utilisant comme technologie de base la bibliothèque d'analyse du C CIL (C Infrastructure Language) développée à l'université de Berkeley. Des détails sont disponibles à l'adresse http://manju.cs.berkeley.edu/cil/. CIL est distribué sous une licence libre nous permettant de le redistribuer à notre convenance. Cette bibliothèque est écrite en OCaml, qui sera donc le langage dans lequel nous implanterons notre projet. La portabilité et les garanties en terme d'efficacité et de sûreté qui nous sont acquises grâce à ce langage sont un atout important. OCaml est un langage pérenne développé par l'INRIA http://www.ocaml.org.
T2.3 : Documentation du noyau
Nous proposerons un manuel et un tutoriel à l'intention du développeur de greffons.
Afin d'évaluer ce sous-projet 2, nous implanterons une fonctionnalité supplémentaire optionnelle qui ne se sera pas contenue dans le noyau et en fonction de la difficulté de cette tâche, nous pourrons juger de la pertinence de notre spécification relativement au besoin d'extensibilté. Cette fonctionnalité devra être simple, mais devra aussi utiliser au maximum l'interaction avec le noyau. L'infrastructure sera ensuite évaluée pendant le développement des greffons prévus dans les autres sous-projets. Aucun autre développement ne peut avoir lieu tant que cette infrastructure ne possédera pas un minimum de fonctionnalités.
Tâche |
Resp. |
Début |
Fin |
Charge (homme/mois) |
Délivrables |
||||||
---|---|---|---|---|---|---|---|---|---|---|---|
CEA |
INRIA |
IRISA |
DA |
AF |
SVDO |
FT |
|||||
T2.0 |
CEA |
M6 |
M7 |
1 |
1 |
|
|
|
|
|
Rapport décrivant l'architecture |
T2.1 |
CEA |
M7 |
M8 |
2 |
2 |
|
|
|
|
|
Rapport de spécification |
T2.2 |
CEA |
M8 |
M10 |
6 |
6 |
|
|
|
|
|
Prototype |
T2.3 |
CEA |
M10 |
M11 |
1 |
1 |
|
|
|
|
|
Documentation |