Analyse et vérification de logiciels embarqués avec structures de mémoire dynamique – AVERILES

1. Introduction

La défaillance de systèmes logiciels embarqués peut avoir des conséquences
économiques énormes. Il est donc nécessaire d'adopter des méthodes formelles
d'analyse et de vérification pour de tels systèmes.
Les méthodes dites de model-checking (basées sur la modélisation par
automate fini) ont eu un succès considérable pour des systèmes à nombre
d'états fini (p.e. les circuits).
Or, les systèmes logiciels comprennent un certain nombre d'aspects
infinis comme ceux liés aux données (par exemple les structures chaînées
dynamiquement, les listes, arbres, etc.).
Un défi actuel est d'étendre les techniques du model-checking à ce type
d'aspects infinis, qui sont difficiles à traiter du aux interactions
complexes par exemple dans des programmes multi-tâches avec utilisation
commune de la mémoire.
Ce type de programmes correspond précisément aux programmes pour lesquels
EDF a besoin de disposer de méthodes et techniques de vérification.
Pour ce type de programme nous visons la vérification d'absence de
défauts intrinsèques (p.e. pas d'erreurs de segmentation).

Pour les systèmes logiciels avec mémoire dynamique (et un nombre
de tâches fixé) le projet développera des modèles adaptés ainsi que les
algorithmes de vérification.
Nous adopterons l'approche du model-checking symbolique déjà utilisée
avec succès pour des systèmes infinis simples (à compteurs, file d'attente
non-bornée, etc.).
Nous concevrons des outils prototypes qui seront intégrés dans
une plateforme commune et expérimentés en utilisant des études de cas
fournis par EDF.

Domaine: Systèmes embarqués
Mots-clé: Méthodes formelles (abstraction, preuves, model-checking,
transformations), Processus et outils de vérification et validation
(preuves, tests, etc.).

2. Objectifs de recherche du projet

Ils existent plusieurs approches pour la vérification des
systèmes logiciels avec mémoire dynamique.
L'approche basée sur l'interprétation abstraite a l'avantage d'être automatique
mais elle est restreinte par rapport aux types de propriétés qu'on peut
vérifier.
L'approche basée sur des logiques est très générale mais demande beaucoup
d'intervention de l'utilisateur.
Nous proposons d'appliquer l'approche du model-checking symbolique
pour les systèmes que nous considérerons pour obtenir des méthodes
générales de vérification qui sont en même temps le plus automatisées que
possible.
Les partenaires académiques du projet ont déjà beaucoup contribué dans
l'approche du model-checking symbolique qui est basée sur la
définition de structures de représentation d'ensembles (infinis) de
configurations d'un système et des algorithmes d'accessibilité
qui calculent des ensembles de configurations atteignables.
Le verrou technologique à lever est de montrer que ces techniques
symboliques peuvent s'appliquer aux systèmes complexes avec mémoire
dynamique et permettent de traiter des cas industriels.
Pour de tels systèmes les membres du projet ont déjà obtenu des résultats
préliminaires encourageants.

3. Objectifs industriels du projet

L'objectif pour le partenaire EDF est de disposer à terme d'outils
performants pour la vérification de logiciels complexes à mémoire dynamique.
En tant que fournisseur de logiciel, le partenaire CRIL Technology
utilise actuellement des outils détectant dynamiquement les fuites mémoires.
L'utilisation de méthodes formelles pour l'analyse et la vérifications
de ces aspects des programmes développées par le projet
permettra la détection des erreurs potentielles au plus tôt dans le cycle
de développement, minimisant ainsi l'impact financier associé.

4. Partenaires, compétences

Le projet regroupe
- trois laboratoires de recherche (LIAFA, LSV et VERIMAG)
reconnus pour leurs travaux dans le domaine de la vérification
qui ont des compétences complémentaires (model-checking symbolique,
approche logique, extraction de modèles)
- un grand groupe industriel (EDF) qu