Directeur de l'action : Ghassan Chehaibar
Personnels Inria :
Inria Rhône-Alpes : Hubert Garavel (CR)
Inria Rennes (Irisa) : Claude Jard, Thierry Jéron, César Viho (CR)
Personnels Bull : Ghassan Chehaibar
Doctorants et stagiaires Inria :
Inria Rhône-Alpes : Radu Mateescu (doctorant MESR)
Mihaela Sighireanu (doctorant MESR)
Bruno Vivien (élève-ingénieur CNAM)
Inria Rennes (Irisa) : Laurence Nedelka (doctorant DYADE)
(décédée en juin 1996 dans un accident
de la circulation)
L'objectif général de l'action VASY porte sur l'amélioration de la qualité et de la productivité de la conception des architectures complexes (multiprocesseurs) par application des méthodes formelles.
L'action VASY a débuté en 1995 par l'étude de l'architecture PowerScale développée par Bull et utilisée dans les stations de travail et les serveurs de la gamme Escala. Un sous-ensemble significatif de cette architecture a été modélisé formellement dans le langage LOTOS (norme ISO 8807), puis l'étude s'est focalisée sur l'abitre de bus de PowerScale, pour lesquel quatre propriétés essentielles de bon fonctionnement ont pu être vérifiées en utilisant la boîte à outils CADP (CAESAR/ALDEBARAN Development Package) développée à l'INRIA Rhône-Alpes. Ce travail a donné lieu à publication [CGM+96].
En 1996, l'action VASY a procédé au regroupement des personnels Bull et INRIA Rhône-Alpes sur le site de Montbonnot. Jusqu'à mi-1997, la cible d'application de l'action VASY est l'architecture multiprocesseur Polykid de Bull, développée à Bull Italie. Trois axes de travail sont identifiés :
1- Maîtrise de la complexité grâce à la spécification formelle en LOTOS du protocole de cohérence de caches de Polykid.
2- Vérification formelle de cette spécification, impliquant la spécification formelle des propriétés à vérifier, la génération des automates de l'architecture et des propriétés au moyen de l'outil CAESAR et la comparaison de ces automates au moyen de l'outil ALDEBARAN. Cet axe de travail requiert une amélioration de CAESAR pour optimiser la génération des automates.
3- Génération de tests à partir de la spécification formelle et d'objectifs formels de tests en utilisant l'outil TGV (Test Generation from Verification Techniques) développé à l'IRISA et l'INRIA Rhône-Alpes. TGV doit servir à générer à la volée des séquences de tests qui seront appliquées pour tester les composants de Polykid. La version existante de TGV ayant été conçue pour manipuler des systèmes de transitions, il faut l'adapter pour traiter des spécifications écrites en Lotos. D'autre part, il faut adapter le format de sortie de TGV à l'environnement réel de test Bull des composants VHDL (appelé SIM1).
En septembre 96, un quatrième objectif nous a été demandé par l'équipe de Bull Italie qui développe l'architecture Polykid:
4- Génération d'un émulateur logiciel d'un composant matériel. Il s'agit de décrire formellement en LOTOS le RCC (Remote Cache Controller) de l'architecture Polykid, puis de traduire automatiquement cette description en langage C au moyen de CAESAR. Le code exécutable ainsi obtenu sera intégré au sein d'un système réel et permettra ainsi de valider la conception du composant RCC.
Enfin, dans une démarche à plus long terme, les doctorants de l'INRIA Rhône-Alpes travaillent sur l'amélioration des techniques de spécification et de vérification:
1- Une première description formelle en LOTOS de l'architecture Polykid a été réalisée. Cette activité de modélisation a permis de soulever certaines questions qui ont été transmises aux architectes de Polykid.
Nous n'avons pu générer l'automate de cette spécification, car sa complexité est à la limite des capacités actuelles des outils (nos expérience montrent que cet automate possède plus de 2 millions d'états et de 7,5 millions de transitions).
C'est pourquoi, il est apparu nécessaire d'améliorer CAESAR de manière à engendrer moins d'états redondants. Pour atteindre cet objectif, le recrutement d'un ingénieur-expert est prévu pour 1997 a l'INRIA Rhône-Alpes.
Dans l'attente de cette amélioration, nous avons suspendu l'activité de vérification formelle en septembre 1996, d'autant plus que la tâche de réalisation de l'émulateur logiciel nous était indiquée comme prioritaire.
Lorsque cette tâche reprendra en 1997, il faudra tenir compte de la nouvelle architecture Polykid (qui a été modifiée entre-temps) et probablement réduire la taille de la spécification (passer de 3 modules et 6 processeurs, à 3 modules et 2 processeurs).
2- Une première version de TGV_Lotos a été implémentée. En septembre 1996, les premières expérimentations avec TGV_Lotos ont prouvé la faisabilité de la génération de séquences de tests à partir de la spécification LOTOS actuelle de Polykid et de quelques objectifs de test.
Le travail actuel peut se définir en trois points :
Pour atteindre ces objectifs, le recrutement d'un ingénieur-expert est prévu pour 1997 à l'IRISA.
3- L'écriture de la spécification formelle de l'émulateur du RCC. Une première version a été livrée début novembre 96, la version complète devant être prête fin décembre 96.
Pour atteindre cet objectif, plusieurs problèmes restent à traiter. Pour obtenir un émulateur exécutable, il faudra interfacer les fragments de code C produits par CAESAR avec certaines structures de données écrites manuellement en C. De plus, le code de l'émulateur devant fonctionner, non pas sous UNIX, mais sous le moniteur de l'environnement Bull de mise au point des machines multiprocesseurs, il convient de modifier le code C produit par CAESAR pour l'adapter aux fonctionnalités plus restreintes de ce moniteur.
1- Les résultats obtenus en 1995 avec l'architecture PowerScale sont
encourageants et on prouvé la faisabilité des objectifs de VASY. Ces résultats ont été présentés au niveau international (conférence FORTE/PSTV'95 et colloque europeen COST-247).
2- L'effort de spécification formelle a permis tout au long de
l'évolution de la spécification informelle de mettre en évidence des ambiguités ou incomplétudes. Dernièrement, les architectes ont modifié le traitement des accès conflictuels dans l'architecture, et nous demandent de vérifier que le nouveau traitement couvre tous les cas.
3- Une première version (incomplète) en LOTOS du composant RCC à emuler
a été traduite en C au moyen de CAESAR et livrée à l'équipe chargée de l'intégration.
@inproceedings{Chehaibar-Garavel-Mounier-Tawbi-Zulian-96,
author = {Ghassan Chehaibar and Hubert Garavel and Laurent Mounier and
Nadia Tawbi and Ferruccio Zulian},
title = {Specification and Verification of the PowerScale Bus
Arbitration Protocol: An Industrial Experiment with LOTOS},
booktitle = {Proceedings of the Joint International Conference on Formal
Description Techniques for Distributed Systems and
Communication Protocols, and Protocol Specification, Testing,
and Verification {FORTE/PSTV}'96 (Kaiserslautern, Germany)},
year = {1996},
editor = {Reinhard Gotzhein and Jan Bredereke},
pages = {435--450},
organization = {IFIP},
publisher = ch,
% address = {},
month = oct,
note = {Full version available as INRIA Research Report~RR-2958},
annote = {PowerScale}
}
@inproceedings{Garavel-96,
author = {Hubert Garavel},
title = {An Overview of the Eucalyptus Toolbox},
booktitle = {Proceedings of the COST 247 International Workshop on
Applied
Formal Methods in System Design (Maribor, Slovenia)},
year = {1996},
editor = {Z. Brezo\v{c}nik and T. Kapus},
% pages = {},
publisher = {University of Maribor, Slovenia},
month = jun,
annote = {EUCALYPTUS, Eucalyptus-2}
}
AUTHOR ={Fernandez, J.-C. and Jard, C. and J\'eron, T. and Viho,
C.},
TITLE = {An Experiment in Automatic Generation of Test Suites for
Protocols with Verification Technology},
JOURNAL = {Science of Computer Programming - Special Issue on
Industrial Relevant Applications of Formal Analysis
Techniques},
EDITOR = {Groote, J.-F. and Rem, M.},
PUBLISHER = {Elsevier Science},
YEAR = {1996}
}
author = "Fernandez, J.-C. and Jard, C. and J\'eron, T. and Viho, C.",
title = "Using on-the-fly verification techniques
for the generation of test suites",
booktitle= "Conference on Computer-Aided Verification (CAV '96), New
Brunswick, New Jersey, USA,
editor= "Alur, A. and Henzinger, T.",
publisher= "Springer",
series= "LNCS 1102",
month = jul,
year = "1996"
Back to the VASY Home Page