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