Sous-projet 2 : Infrastructure générique

Description du sous-projet, responsable, partenaires

Développement du noyau logiciel du projet.

Début : M6

Fin : M11

Responsable : CEA

Participants : CEA, INRIA

Objectifs du sous-projet

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).

Détails des réalisations et échéances

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.

Critère d'évaluation du résultat et de décision de poursuite du sous-projet

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