next up previous
Next: Sujet : L(A)=L(B)? Up: Sujets de thèse autour Previous: Sujet : Extensions de

Sujet : Techniques de vérification et de génération de séquences de test

 

Fiche signalétique

Responsable Richard Castanet 05 56 84 69 01 Richard.Castanet@labri.u-bordeaux.fr
Collaborateur Pierre Castéran 05 56 84 69 31 Pierre.Casteran@labri.u-bordeaux.fr
Equipe MVTsi
Titre
Techniques de vérification et de génération de séquences de test.
Catégorie Théorique et expérimentale
Position/AltaRica Outil satellite
Moyen terme
Financement Bourse de thèse MENRT
Frais de fonctionnement sur projet FORMA

Présentation du sujet

Contexte

L'équipe MVTsi (Modélisation, vérification et test de systèmes informatisés) possède des compétences dans les domaines de la vérification, du test et de la sûreté de fonctionnement. Les techniques de preuve représentent une compétence au LaBRI venant conforter le domaine de recherche lié au sujet de thèse. Les techniques les plus récentes dans la génération de séquences de test utilisent des techniques liées à la vérification des systèmes. Une démarche connue des milieux de la recherche et de plus en plus acceptée par les industriels est la suivante : spécification formelle d'un système, vérification formelle et génération automatique de séquences de test qui seront injectées dans le système implémenté. Le contexte général du sujet de recherche s'inscrit dans un projet intitulé FORMA (CNRS-MENSR) en collaboration avec l'ENS-Cachan, l'Irisa de Rennes, Verimag de Grenoble et le CNET-Lannion. Ce sujet sera aussi lié au projet AltaRica du LaBRI.

Travail demandé

A partir de descriptions effectuées dans des langages de spécification formelle (en général SDL ou AltaRica), il s'agit de vérifier ou de prouver des propriétés et de permettre des générations automatiques de séquences de test selon des objectifs de test définis.

On s'intéressera à des approches prenant en compte une spécification par modules et en étant soit descendantes : vérification ou preuves de propriétés globales et génération de test global avec vision des implications sur les modules internes soit descendantes : vérification ou preuve d'un module de la spécification et génération de tests locaux avec intégration dans un test global. Des approches mixtes sont souhaitables: aide à la vérification à l'aide de techniques de preuve, aide à la génération automatique de tests à l'aide de techniques de vérification et de preuve.

Il faudra concevoir un outil global permettant à partir de spécifications formelles (SDL, AltaRica ...) de spécifier des propriétés (locales ou globales), de faire des vérifications et de générer automatiquement des tests.

Environnement

Utilisation des outils

afin de traiter des exemples de :


next up previous
Next: Sujet : L(A)=L(B)? Up: Sujets de thèse autour Previous: Sujet : Extensions de

Equipe Modélisation, Vérification et Test des systèmes informatisés
Fri May 15 10:32:44 CEST 1998