Le projet AVERILES est supporté par le RNTL (Réseau National des Technologies Logiciels) de l'ANR (Agence Nationale de la Recherche).
Description du projet :
Le but de ce projet est de développer des techniques avancées pour l'analyse et la vérification de logiciels embarqués complexes. Le projet vise en particulier le traitement de programmes multi-tâches avec allocation de mémoire dynamique et manipulation de pointeurs. Il s'agit de développer une approche outillée pour vérifier :
- l'absence de défauts intrinsèques dans la manipulation de la mémoire ;
- des propriétés sur la structure de la mémoire pour de genre de logiciels embarqués complexes.
Des exemples de tels programmes sont ceux utilisés par EDF dans des systèmes d'aide à l'exploitation de production d´énergie.
Objectifs du projet
Ce projet comprend plusieurs volets :
- Définition de modèles adéquates pour les programmes analysés
- Conception de nouvelles techniques algorithmiques pour la vérification symbolique de tels modèles
- Développement de prototypes d'outils implémentant des algorithmes de vérification
- Intégration des outils dans une plate-forme commune
Dans le cadre du projet AVERILES, différents outils permettant de vérifier des programmes manipulant dynamiquement la mémoire ont été développés. Voilà la liste des outils existants actuellement :
- Pour des programmes manipulant des listes simplement chaînées : L2CA
- Pour des programmes manipulant des listes simplement chaînées:TOPICS
- Pour des programmes manipulant des structures de données plus complexes : ARTMC
Ces outils seront regroupés au sein d'un outil servant à les interfacer.
De plus, une base de données commune d'exemples de programmes à analyser est disponible ici.
Le projet RNTL AVERILES rassemble trois laboratoires français: le VERIMAG à Grenoble, le LSV à Cachan et le LIAFA à Paris. Participent également au projet EDF R&D et ALYOTECH. Dans le tableau qui suit, les noms en gras indiquent les responsables du projet.
Réunions pleinières
- 13 Octobre 2009 (LIAFA)
- 27 Mai 2009 (LIAFA)
- 17 Novembre 2008 (LIAFA)
- 11 Juin 2008 (LIAFA)
- 18 Février 2008 (LIAFA)
- 12 Juillet 2007 (LSV)
- 5-6 Mars 2007 (LIAFA) (Réeunion coorganisée avec le projet ANR AVERISS)
- 6 Novembre 2006 (LIAFA)
- 7 Juin 2006 (LIAFA)
- 15 Mars 2006 (LIAFA)
- 23 Janvier 2006 (LIAFA)
Réunions techniques
- 20 Mai 2008 : Discussion Modèles + Concurrence (LSV)
- 20/21 Mars 2008 : Discussion sur la concurrence (VERIMAG)
- 23 Mai 2007 : Discussion sur les modèles (LIAFA)
- 5 Avril 2007 : Discussion sur les modèles (VERIMAG)
- 28 Novembre 2006 : Discussion sur l'étude de cas (LIAFA)