Plate-forme Systèmes et Logiciels Critiques

Projet OTEST

Plan

gorigh.gifPrésentation

gorigh.gifButs et moyens

gorigh.gifJSLC 2000

gorigh.gifJSLC 2001

gorigh.gifProjets-pilote

gorigh.gifClub des Partenaires

gorigh.gifNous contacter

gorigh.gifLiens


Projet OTEST




Le projet OTEST s'inscrit dans le cadre  de la validation des systèmes distribués, et notamment pour des applications issues du domaine des télécomunications ou du contrôle/commande. Plus précisement, le but du projet est la  génération automatique d'objectifs de tests à  partir d'une spécification SDL assurant une couverture comportementale du système considéré.  La solution proposée reposera sur une combinaison de différentes techniques et outils dont le model-checking (outils IF et TGV), l'exécution symbolique (outil Agatha) et  le calcul d'abstractions (outil InVeSt).

Acteurs

Le projet regroupe deux partenaires :
 
  • le CEA-LETI, dont le représentant technique pour le projet est Jean-Pierre Gallois ;
  • le laboratoire VERIMAG, dont les représentants techniques pour le projet sont Yassine Lakhnech et Laurent Mounier.

    • Objectifs

    L'objectif général du projet est de renforcer les méthodes et outils existants en matière de validation des systèmes distribués, et notamment dans le domaine des télécomunication et du contrôle/commande. Il concerne plus précisement la génération automatique de test à partir d'une spécification formelle exécutable, exprimée par exemple en langage SDL qui est la norme internationale pour les protocoles de communication.

    Une approche  efficace pour la génération automatique de séquences de test  à partir de spécifications de ce type est désormais opérationnelle, avec notamment l'outil TGV (Verimag/Irisa) ou encore l'outil commercial TestComposer (Telelogic) qui en est derivé. Deux problèmes pratiques subsistent toutefois pour utiliser ces outils :

  • le choix des objectifs de test à partir desquels les cas de test seront générés ;
  • le traitement des donnés dans les cas de test, afin de générer des cas de test "symboliques" (dont les variables pourront être instanciées lors de l'exécution du test).

    •  

     
     
     

    Le projet Otest a pour objectif d'améliorer ces deux aspects en proposant notamment une technique de génération d'objectifs de test au moyen d'une exécution symbolique de la spécification et permettant d'en assurer une couverture comportementale suivant le critère de la couverture de chemin.
     

    Démarche proposée

    La démarche envisagée s'appuie directement sur les compétences et les outils déjà développés par les deux partenaires.
    Elle consiste notamment :
  • à connecter l'outil d'exécution symbolique Agatha (CEA-Leti) au format intermédiaire IF (Verimag) permettant de représenter des spécifications SDL produite par l'outil commercial Object-Geode (Telelogic) ;
  • à intégrer dans cet environnement des techniques d'abstractions issues de l'outil InVeSt (Verimag), nécessaires pour garantir la correction des exécutions symboliques ainsi générées.

    •  

     
     
     

    Le plan de travail proposé consiste en une première phase (d'une durée d'un an) pendant laquelle la connection IF-Agatha sera realisée puis validée sur une étude de cas nécessitant uniquement des abstractions simples. Dans une deuxième phase ces resultats seront alors étendus à des exemples plus généraux, nécessitant des techniques d'abstractions plus sophistiquées, et validés au moyen d'une seconde étude de cas.
     

    Résultats attendus

    A l'issue de la premiere année l'outil Agatha pourra accepter en entrée des spécifications SDL (via le format intermediaire IF) et générer des objectifs de test symboliques à partir de cette spécification.