Rapport d'activité Dyade/VASY 1997

Sommaire

Introduction
Équipe
Programme de travail
État d'avancement
Résultats et transferts industriels
Références

Introduction

Cette page est un extrait du rapport d'activité complet de l'action de développement DYADE, pour l'année 1997. Elle est composée des parties qui concernent l'action VASY.

Équipe

Directeur de l'action	Ghassan Chehaibar (Bull)
Projets INRIA	VASY-RA (Grenoble) PAMPA (Rennes)
Personnels INRIA	Hubert Garavel (Chargé de Recherche) Claude Jard (Chargé de Recherche, CNRS) César Viho (Chargé de Recherche)
Ingénieur Expert	Mark Jorgensen
Post-doctorants INRIA	Hakim Kalhouche (à partir d'août 1997)
Personnels Bull	Massimo Zendri (à partir de juillet 1997)

L'objectif de l'action VASY est l'expérimentation industrielle de l'utilisation de méthodes formelles dans le processus de développement de systèmes complexes. Les résultats attendus sont de montrer que les méthodes formelles améliorent la qualité et la productivité de la conception des systèmes.

En vue d'un transfert technologique dans Bull, notre cible d'application, depuis 1995, est le développement des architectures des multiprocesseurs UNIX conçus par le centre de développement de Bull à Pregnana (Milan).
Plus particulièrement, depuis 1996, la cible d'application de l'action VASY est le protocole de cohérence des caches de l'architecture multiprocesseur CC-NUMA développée a Bull-Pregnana.

État d'avancement

Le programme de travail en 96/97 comprend trois thèmes :

1) Aide à la conception et à la mise au point du protocole de cohérence de caches d'un grand serveur multiprocesseurs (Polykid).

À partir de la spécification servant de base au développement de l'architecture de Polykid, nous construisons une spécification formelle et vérifions certaines propriétés formellement.
Cette activité permet d'améliorer la qualité de la spécification de référence, en clarifiant les ambiguïtés et soulevant des problèmes tels que des hypothèses implicites non documentées ou bien des erreurs de comportement du protocole.

Nous utilisons le langage de spécification formelle LOTOS (norme ISO 8807) et la boîte à outils CADP développée par l'INRIA Rhône-Alpes, Verimag (et intégrant dernièrement des outils développés à l'INRIA Sophia-Antipolis).
Une nouvelle description formelle en LOTOS du protocole de cohérence des caches de Polykid a été réalisée. Cette activité de modélisation a permis de soulever 13 problèmes dans la spécification de référence : 6 hypothèses non documentées et 7 erreurs de comportement (1 blocage et 7 pertes de cohérence des caches). Ces erreurs ont été trouvées avant la phase de tests des composants réels. Fin 96, nous avions déjà trouvé 1 blocage et 6 autres incomplétudes dans la spécification.
Les architectes de Polykid ont proposé des solutions aux erreurs. Ces corrections ont été incorporées dans la description formelle en cours : puis nous avons vérifié formellement, au moyen des outils de CADP, qu'elle ne contenait plus aucune erreur. Pour s'assurer de la précision de cette description, nous y avons introduit deux des sept erreurs trouvées et nous avons vérifié que les outils les détectaient.
Nous avons réussi à générer l'automate correspondant en utilisant les dernières techniques de vérification compositionnelle introduites dans CADP. Néanmoins, cette description est simplifiée et réduite à deux modules, et il est nécessaire de traiter des configurations plus grandes et plus détaillées. Pour cela, nous travaillons actuellement à :

rechercher de meilleures abstractions de modélisation,
améliorer la génération d'automates par le compilateur CAESAR pour produire moins d'états.

La boite à outils CADP a été considérablement améliorée, durant 1997 :

le compilateur de LOTOS CAESAR est beaucoup plus rapide (selon les cas, la vitesse est multipliée par 2 à 160),
de nombreuses bogues ont été corrigées,
de nouveaux outils de vérification compositionnelle ont été intégrés (projector et des2aut développés à Verimag),
de nouveaux outils de vérification développés à l'INRIA Sophia-Antipolis ont été intégrés (Fc2Tools),
l'interface graphique de CADP a été rendue plus ergonomique.

2) Génération automatique de cas de tests.

Il s'agit de générer des cas de tests à partir de la spécification formelle et d'objectifs formels de tests en utilisant l'outil TGV (Test Generation using Verification technology) développé à l'IRISA et Verimag.
TGV doit servir à générer des séquences de tests qui seront appliquées pour tester que les composants de Polykid sont conformes à la spécification formelle.
Cette approche réduit le coût de l'activité de tests : le cas de test, généré automatiquement, envoie des stimuli à l'implémentation et vérifie que ses réactions sont conformes à la spécification ; ce qui évite d'écrire manuellement toutes les interactions d'un cas de test et de développer un vérificateur des résultats.
De plus, cette technique permet de concevoir des tests plus complexes et d'assurer une meilleure couverture par rapport aux objectifs de tests.
La version initiale de TGV ayant été conçue pour manipuler des systèmes de transitions, il a fallu l'adapter pour traiter des spécifications écrites en LOTOS. Il reste à développer des outils supplémentaires pour adapter le format de sortie de TGV à l'environnement réel de test Bull des composants VHDL.

Les algorithmes et les interfaces de la première version de TGV_Lotos implémentée durant 96 ont été améliorés pour prendre en compte les caractéristiques de LOTOS et de l'environnement réel de tests. Une série de tests abstraits a été produite à partir de la première spécification formelle du protocole de cohérence de caches de Polykid.

L'outil TGV_Lotos a été installé mi-97 à l'INRIA Rhône-Alpes où l'on maîtrise bien son utilisation maintenant. Dans un premier temps, nous développons une solution qui automatise la pratique actuelle des tests de premier niveau à Bull-Pregnana qui se font en mode batch. Mais, comme l'avantage essentiel de TGV est de permettre des tests interactifs, nous avons l'intention de mettre courant 98 une solution de test interactive qui permettra de réaliser une plus grande couverture de tests (ceci demandera des modifications dans l'environnement actuel de tests de premier niveau de Bull-Pregnana).

Le travail en cours peut se définir en deux points :

écrire une nouvelle spécification LOTOS du protocole de cohérence de caches. Il est nécessaire d'avoir un modèle contenant tous les signaux d'entrée/sortie de la plate-forme de tests, donc plus complet qu'un modèle dédié à la vérification.
développer un ensemble d'outils qui font correspondre les cas des tests abstraits générés par TGV à la pratique actuelle des tests de premier niveau à Pregnana.

3) Génération d'un émulateur logiciel d'un composant matériel

Ce travail fait suite à une demande faite par l'équipe de Bull-Pregnana qui développe l'architecture. Il s'agit de décrire formellement en LOTOS un composant de l'architecture, le RCC, puis de traduire automatiquement cette description en langage C au moyen de CAESAR. Le code exécutable ainsi obtenu est intégré au sein d'un système réel et permet ainsi de valider la conception du composant RCC.

Le programme C d'émulation a été réalisé d'abord par traduction d'une spécification LOTOS en C et une importante couche de fonctions directement écrites en C et appelées à partir du programme LOTOS. Quand les tests du prototype ont commencé, le programme obtenu fonctionnait mais sa vitesse d'exécution était très inférieure à ce qui était exigé par l'environnement de tests. Il a fallu réécrire la partie contrôle de LOTOS en C, tout en gardant la partie données de LOTOS. Ceci a divisé le temps d'exécution par 60. Puis le code C obtenu a été optimisé : temps encore divisé par 30. A la fin, le programme source contenait 8000 lignes de C et 1500 lignes de LOTOS.

Néanmoins, les problèmes de vitesse d'exécution du code généré par le compilateur LOTOS, ont entraîné un travail important d'amélioration des performances de CAESAR (le compilateur de LOTOS) qui a aussi bénéficié à la génération d'automates pour la vérification (voir ci-dessus). L'activité de prototypage à partir d'une spécification en LOTOS a soulevé un autre problème : la sémantique de LOTOS est fondée sur le paradigme fonctionnel ; alors que, dans l'émulation, nous avions de grandes structures de données qu'on a besoin de modifier par des fonctions à effets de bord. De plus, nous avions des fonctions qui dépendaient des variables globales de l'environnement, qui étaient donc déclarées constantes en LOTOS. Toutes ces contraintes nous ont obligé à utiliser certaines constructions mal maîtrisées et qui ont compliqué l'écriture du programme LOTOS.

Résultats et transferts industriels

Depuis fin 96, la spécification et vérification formelle de l'architecture Polykid en cours de développement, à partir de la spécification informelle, ont été faites en étroite collaboration avec les architectes de Bull-Pregnana, qui ont jugé cette activité très profitable.
Le programme d'émulation du composant RCC a permis de mettre en place une activité supplémentaire de validation de l'architecture, complémentaire des autres activités de tests et simulation.
Une personne supplémentaire a été détachée de Bull-Pregnana dans VASY pour une durée de deux ans (à partir du 1er juillet 1997) pour acquérir une expertise en méthodes formelles et contribuer à leur application aux systèmes développés à Pregnana.

Références

CADP'97 - Status, Applications and Perspectives
H.Garavel, M.Jorgensen, R.Mateescu, C.Pecheur, M.Sighireanu, B.Vivien.
in Proceedings of the 2nd COST-247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatie), I.Lovrek (red.), juin 1997

Une expérience de génération automatique de tests pour un protocole de cohérence de caches
C.Jard, T.Jeron, P.Morel, C.Viho.
Actes de la conférence TESTING'97 sur le test de logiciels, Paris, juin 1997

Back to the VASY Home Page