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 |
| |||
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 |
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.
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.
Utilisation des outils
afin de traiter des exemples de :