Français Anglais
Accueil Annuaire Plan du site
Production scientifique
Contrat de l'équipe Test Formel et Exploration de Systèmes
HOL-TESTGEN XT

DIGITEO
Févr. 2009 - Janv. 2012

Equipe : Test Formel et Exploration de Systèmes
Responsable : WOLFF Burkhart

Gestionnaire : 
Organisme gérant : Université Paris XI

Un generateur pour des donnees de test sur base de HOL

Chaire d'excellence Université Paris XI.
Le but de ce projet de recherche est d'augmenter l'espace d'états maniables du système HOL-TestGen de plusieurs ordres de grandeurs. Ainsi, la technologie de génération des tests par HOL-TestGen aura encore plus de potentiel pour
des applications industrielles dans des scénarios réalistes
pour le test à base de modèles. Nous proposons une combinaison de 3 techniques pour obtenir ce but:
- On va intégrer dans HOL-TestGen des systèmes de preuve automatisés de type SAT solver, en particulier Z3.
- Avec la complexité croissante, il y aura certaines contraintes insolubles. On va générer du code optimisé pour ce genre de contraintes et essayer de les résoudre par "generate and test".
Il faudra adapter cette méthode surtout pour des scenarios
de systèmes réactifs.
- Le succès d'une méthode de génération de tests dépend de façon critique des règles dérivées de la théorie du domaine
du test. Ce genre de règles permet souvent très tôt de détecter des contraintes insolubles. On va explorer des méthodes automatisées pour générer ce genre de règles.

Activités de recherche
  SAT
  Vérification
  Test de Logiciels
  Langages d'ordre supérieur
  Méthodes Formelles de Génie Logiciel

Membres LRI
WOLFF Burkhart


Pour en savoir plus : http://www.lri.fr/~wolff/research.html#section1b
Contrats
° IUF
FABIO MARTIGNON
SUBVENTION

° DIGISCOPE UPS
INFRASTRUCTURE HAUTE PERFORMANCE POUR LA VISUALISATION INTERACTIVE ET COLLABORATIVE
ANR

° DIGISCOPE CNRS
INFRASTRUCTURE HAUTE PERFORMANCE POUR LA VISUALISATION INTERACTIVE ET COLLABORATIVE
ANR

° ATOS/BULL
CONTRAT ATOS/BULL
INDUSTRIEL

° LCHIP
LCHIP