Associer des techniques de preuve et de résolution de contraintes pour la construction d'abstractions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Associer des techniques de preuve et de résolution de contraintes pour la construction d'abstractions

Résumé

Cet article présente une méthode de génération assistée de tests. Elle applique des critères dynamiques de sélection des tests (TP) sur un modèle formel comportemental (M) utilisé auparavant, par exemple par LTG, pour générer des tests fonctionnels à partir de critères statiques de sélection. On peut appliquer à M un critère dynamique de sélection TP mais ceci nécessite de représenterM par un automate. Pour des applications réelles, sa taille en nombre d'états et de transitions est beaucoup trop grande (voir infinie) pour être utilisable. Nous proposons une méthode pour extraire une abstraction de M à partir d'un objectif de test TP. Nous effectuons un produit synchronisé de cette abstraction avec TP afin de cibler les exécutions du système sous test qui satisfont TP. Puis nous générons des tests abstraits symboliques à partir de ce modèle réduit en appliquant les critères de couverture tous les états ou toutes les transitions. Cet ensemble de tests est valué à partir de M, concrétisé puis exécuté sur l'implémentation sous test. Cette méthode est proposée pour compléter la méthode BZ-TT de génération de tests à partir de critères statiques de sélection. L'utilisateur obtient des tests complémentaires en fournissant un critère dynamique de sélection. La méthode réutilise M, la couche de concrétisation des tests et l'infrastructure d'exécution des tests. L'originalité de l'approche est de construire une abstraction du modèle issue automatiquement de l'analyse statique d'un objectif de test formalisant des besoins de test d'une propriété dynamique du système.
Fichier principal
Vignette du fichier
bjmb10_np.pdf (405.53 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00563329 , version 1 (04-02-2011)

Identifiants

  • HAL Id : hal-00563329 , version 1

Citer

Pierre-Christophe Bué, Jacques Julliand, Pierre-Alain Masson, Fabrice Bouquet. Associer des techniques de preuve et de résolution de contraintes pour la construction d'abstractions. 10èmes Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'10, Jun 2010, Poitiers, France. pp.11--25. ⟨hal-00563329⟩
125 Consultations
71 Téléchargements

Partager

Gmail Facebook X LinkedIn More