Rapport d'activité Dyade/VASY 1996

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 1996. Elle est composée des parties qui concernent l'action VASY.

Équipe

Directeur de l'action	Ghassan Chehaibar (Bull)
Projets INRIA	SPECTRE (Grenoble) PAMPA (Rennes)
Personnels INRIA	Hubert Garavel (Chargé de Recherche) Claude Jard (Chargé de Recherche, CNRS) Thierry Jéron (Chargé de Recherche) César Viho (Chargé de Recherche)
Doctorants INRIA	Radu Mateescu Mihaela Sighireanu Laurence Nedelka (décédée en Juin 1996 dans un accident de la circulation)
Stagiaire INRIA	Bruno Vivien (élève-ingénieur CNAM)

Programme de travail

L'action VASY a pour objectif de faciliter la conception de l'architecture de systèmes matériels complexes (cluster de multiprocesseurs) par application des méthodes formelles.

L'action VASY a débuté en 1995 par la vérification de l'architecture d'un système existant. Un sous-ensemble significatif de cette architecture a été modélisé formellement dans le langage LOTOS (norme ISO 8807); l'étude s'est ensuite focalisée sur le mécanisme d'arbitrage de bus, pour lequel quatre propriétés essentielles de bon fonctionnement ont été vérifiées à posteriori 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.

La cible de l'action est l'étude d'une architecture multiprocesseur complexe selon les trois axes suivants :

Maîtrise de la complexité grâce à la spécification formelle en LOTOS d'un protocole de cohérence de caches.
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.
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 l'architecture cible. 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).

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 :

contribution à la définition de la future norme Extended-LOTOS, qui améliore significativement le langage LOTOS, notamment dans la perspective d'une utilisation industrielle.
étude et implémentation d'une extension du µ-calcul modal par des variables typées, ce qui devrait permettre de vérifier plus aisément des propriétés portant sur des signaux avec valeurs, comme celles vérifiées pour l'architecture cible [CGM+96].

État d'avancement

Une première description formelle en LOTOS d'une architecture multiprocesseur a été réalisée. Cette activité de modélisation a permis de soulever certaines questions qui ont été transmises à l'équipe de réalisation.

La génération de l'automate de la spécification a posé problème : 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).

De fait il est apparu nécessaire d'améliorer CAESAR de manière à engendrer moins d'états redondants.

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 l'architecture cible et de premiers objectifs de test.

L'évolution de l'activité peut se définir en trois points :

définir de nouveaux objectifs de tests, en étudiant particulièrement la question de leur pertinence,
améliorer les performances de TGV_Lotos (génération à la volée, tau-abstraction et déterminisation, etc) pour pouvoir traiter des spécifications plus complètes,
étudier l'utilisation des séquences de tests générées par TGV_Lotos sur la plate-forme de test de l'architecture cible.

Résultats et transferts industriels

Les résultats obtenus sont très encourageants et ont 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 Européen COST-247).

L'effort de spécification formelle a permis tout au long de l'évolution de la spécification informelle de mettre en évidence des ambiguïtés ou incomplétudes. Dernièrement, les architectes ont modifié le traitement des accès conflictuels dans l'architecture et ont demandé à l'équipe Dyade de vérifier la complétude de la définition.

Une première version (incomplète) en LOTOS du composant RCC a été traduite en C au moyen de CAESAR et livrée à l'équipe chargée de l'intégration.

Références

An Overview of the Eucalyptus Toolbox
Hubert Garavel
Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, Z. Brezovnik and T. Kapus, University of Maribor, Slovenia, Eucalyptus-2, June 1996.

An Experiment in Automatic Generation of Test Suites for Protocols with Verification Technology
J.-C. Fernandez and C. Jard, T. Jéron, C. Viho
Science of Computer Programming, Special Issue on Industrial Relevant Applications of Formal Analysis Techniques, Groote, J.-F. and Rem, M., Elsevier Science, 1996.

Using on-the-fly verification techniques for the generation of test suites
J.-C. Fernandez and C. Jard, T. Jéron, C. Viho,
Conference on Computer-Aided Verification (CAV '96), New Brunswick, New Jersey, USA, Alur A. and Henzinger T., Springer, LNCS 1102, July 1996.

Specification and Verification of the PowerScale Bus Arbitration Protocol : An Industrial Experiment with LOTOS
Ghassan Chehaibar and Hubert Garavel, Laurent Mounier, Nadia Tawbi, Ferruccio Zulian
Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, Protocol Specification, Testing and Verification, FORTE/PSTV'96 (Kaiserslautern, Germany), 1996, Ed. Reinhard Gotzhein and Jan Bredereke, pp 435--450, IFIP, October, Full version available as INRIA Research Report, RR-2958.

Back to the VASY Home Page