Bull INRIA

Rapport d'activité Dyade/VASY 1998

Sommaire

Introduction

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

Équipe

Directeur de l'action Massimo Zendri (Bull)
Projets INRIA VASY (Grenoble)
PAMPA (Rennes)
Personnels INRIA Hubert Garavel (Chargé de Recherche)
César Viho (Maître de conférences)
Personnels CNRS Claude Jard (Chargé de Recherche)
Ingénieur Expert Christophe Discours (à partir d'avril 1998)
Post-doctorant INRIA Hakim Kalhouche

Programme de travail

L'action VASY s'inscrit dans la problématique de la conception de systèmes sûrs par l'utilisation de méthodes formelles. Plus précisément, nous nous intéressons à tout système (matériel, logiciel, télécommunications) faisant intervenir du parallélisme asynchrone, une modélisation du parallélisme basée sur la sémantique d'entrelacement (interleaving semantics) et bien adaptée à la description de systèmes répartis.

Pour la conception de systèmes sûrs, nous préconisons l'utilisation de techniques de description formelles, complétées par des outils informatiques adaptés, offrant des fonctionnalités de simulation, prototypage rapide, validation et vérification formelle et génération des tests.

Parmi les différentes approches existantes pour la vérification, nous concentrons nos efforts sur la vérification "basée sur les modèles" (model-checking) qui recouvre un grand nombre de techniques spécialisées.

Les logiciels utilisés et/ou développés par l'action sont la boîte à outils CADP et l'algorithme de génération des tests TGV. L'objectif de l'action VASY est d'appliquer nos outils pour la vérification d'architectures multiprocesseurs.

État d'avancement

La description LOTOS modélisant le fonctionnement de l'architecture multiprocesseur CC-NUMA POLYKID élaborée en 1997 a été complétée, afin de prendre en compte les transferts de données ainsi que d'autres détails internes qui ont permis de disposer d'une description plus adaptée aux exigences de la génération de test. Pour permettre une évaluation des améliorations effectuées ainsi qu'une comparaison des différents outils, un benchmark a été mis en place. Cela a mis en évidence la nécessité d'un outil de simulation plus puissant (OCIS) pour faciliter l'écriture des spécifications ainsi qu'un outil (SVL) pour faciliter l'application d'une technique de vérification compositionelle qui devrait permettre de résoudre les problèmes de complexité. On a ensuite utilisé d'une façon intensive l'outil TGV, pour générer quelques centaines de cas de test, qui couvrent le plan de test fixé pour Polykid.

Des modifications au coeur de l'outil TGV ont été nécessaires notamment pour résoudre les problèmes liés à la génération des boucles dans les tests. Un environnement de simulation a été mis en place à Grenoble qui intègre l'environnement développé à Pregnana avec un outil développé à Rennes pour rendre exécutables les tests abstraits précédemment obtenus par TGV. L'application des tests générés sur le modèle VHDL du chip RCC a mis en évidence 5 cas d'incohérences entre la spécification et le comportement du RCC. Ce travail a donné lieu à deux publications.

Un essai a été conduit sur la possibilité de générer des tests généralisés, capables d'explorer une partie de l'espace d'états du système qu'on vérifie face à une propriété abstraite. Cette approche permet de générer automatiquement des suites de tests plus importantes qui ciblent une propriété donnée et qui sont plus faciles à déboguer par rapport aux tests générés avec la méthodologie aléatoire qui est l'état de l'art dans le domaine. Une réflexion plus approfondie sur le sujet est en cours à Rennes. Depuis septembre une collaboration est mise en place pour appliquer la technologie au développement d'une nouvelle architecture CC-NUMA développée par le centre R&D Bull des Clayes sous Bois.

Résultats et transferts industriels

L'activité de génération test appliquée à l'architecture Polykid a donné des résultats intéressants, cette activité sera appliquée à une nouvelle architecture développée à Bull Les Clayes pour confirmer son efficacité. Un transfert technologique plus important est prévu pour la seconde moitié de 1999.

Références

An Industrial Experiment in Automatic Generation of Executable Test Suites for a Cache Coherency Protocol
H. Kahlouche, C. Viho, M. Zendri
in Proceedings of IWTCS'98 "International Workshop on Testing of Communicating Systems", Tomsk, Russia, September 1998

Hardware testing using a communication protocol conformance testing tool
H. Kahlouche, C. Viho, M. Zendri
in Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99), Amsterdam, the Netherlands, March 1999

Back to the VASY Home Page