déposé avant le
sur le site web de l'ACI1:
envoyé par voie postale
avec les signatures requises
| Nom du Projet : (maximum 20 caractères) |
| DYNAMO |
| Titre du Projet : (maximum 3 lignes) |
| Analyse de Logiciels Concurrents Embarqués: Mémoire et Contrôle Dynamique |
| Type du Projet2: | |||
| Projet de recherche | Projet de recherche | Projet de recherche | Autre |
| multi-thématiques | avec infrastructure | ||
| X | |||
| Durée du projet3: 3 ans |
| Description courte du Projet : (une demi-page maximum) |
| La vérification de logiciels concurrents embarqués est actuellement un des thèmes
de recherche majeurs dans le domaine des technologies du logiciel. La complexité
grandissante et le caractère souvent critique de ces systèmes rend nécessaire le
développement de méthodes et d`outils de conception et de validation permettant de
garantir leur sûrete de fonctionnement. La vérification automatique de logiciels
complexes pose de nombreux problèmes non triviaux, qui sont hors du portée des
techniques et outils actuelles. Les sources de complexité sont les suivantes:
- Structures de données dynamiques : d`une part la taille de la mémoire peut croître arbitrairement et d`autre part sa structure peut changer dynamiquement au cours de l`exécution d`un programme. - Paramètres et variables sur des domaines infinis : les procédures ont de manière générale des paramètres, et ils manipulent des variables locales et/ou globales. Les domaines de valeurs de ces paramètres et variables peuvent être infinis (par exemple les entiers). - Concurrence: des processus parallèles peuvent communiquer entre eux selon différents schémas (variables partagées, rendez-vous, broadcast, etc.). Ceci pose de problèmes de blocage, d`exclusion mutuelle, etc. Les langages couramment utilisées (comme JAVA) contiennent des primitives qui permettent de programmer la synchronisation des processus au niveau du logiciel. - Structures de contrôle dynamiques: des processus parallèles peuvent être créés dynamiquement et de manière non bornée. De plus, des procédures peuvent être appelées récursivement, de manière non bornée. Il est possible donc d`avoir des piles de contextes de retour ayant des tailles arbitrairement grandes (on doit avoir une pile par processus parallèle en cours d`exécution). |
| Très souvent, l`analyse des programmes doit se faire en tenant compte simultanément
d`une combinaison de ces aspects. Par exemple, la vérification de propriétés sur la
structure de la mémoire ou sur la consommation de ressources mémoire ne peut ignorer
la possibilité de création dynamique de processus parallèles ou celle d`avoir des
appels récursifs, comme elle ne peut se passer d`intégrer un raisonnement sur
les valeurs possibles des paramètres et des variables manipulées.
En général, les techniques existantes permettent seulement de traiter un aspect a la fois. L`action vise à développer des méthodes efficaces permettant de vérifier et d´analyser de manière automatique des programmes comprenant des combinaisons des aspects cités plus haut. Nous comptons appliquer les techniques à la vérification de programmes JAVA, un langage de programmation où tous les difficultés de logiciels sont présentes. |
| Coordinateur du projet : | ||
| Nom | Prénom | Laboratoire (sigle éventuel et nom complet) |
| Yovine | Sergio | VERIMAG UMR 5104 |
| Organisme de rattachement financier pour le présent projet : |
| CNRS |
| Équipes ou laboratoires partenaires (nom complet et éventuellement sigle)4 |
| Laboratoire d'Informatique Algorithmique (LIAFA) |