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

Content Provider	Semantic Scholar
Author	Bué, Pierre-Christophe Julliand, Jacques Masson, Pierre-Alain Bouquet, Fabrice
Copyright Year	2010
Abstract	Cet article presente une methode de generation assistee de tests. Elle applique des criteres dynamiques de selection des tests (TP) sur un modele formel comportemental (M) utilise auparavant, par exemple par LTG, pour generer des tests fonctionnels a partir de criteres statiques de selection. On peut appliquer a M un critere dynamique de selection TP mais ceci necessite de representerM par un automate. Pour des applications reelles, sa taille en nombre d'etats et de transitions est beaucoup trop grande (voir infinie) pour etre utilisable. Nous proposons une methode pour extraire une abstraction de M a partir d'un objectif de test TP. Nous effectuons un produit synchronise de cette abstraction avec TP afin de cibler les executions du systeme sous test qui satisfont TP. Puis nous generons des tests abstraits symboliques a partir de ce modele reduit en appliquant les criteres de couverture tous les etats ou toutes les transitions. Cet ensemble de tests est value a partir de M, concretise puis execute sur l'implementation sous test. Cette methode est proposee pour completer la methode BZ-TT de generation de tests a partir de criteres statiques de selection. L'utilisateur obtient des tests complementaires en fournissant un critere dynamique de selection. La methode reutilise M, la couche de concretisation des tests et l'infrastructure d'execution des tests. L'originalite de l'approche est de construire une abstraction du modele issue automatiquement de l'analyse statique d'un objectif de test formalisant des besoins de test d'une propriete dynamique du systeme.
File Format	PDF HTM / HTML
Alternate Webpage(s)	https://publiweb.femto-st.fr/tntnet/entries/426/documents/author/data
Language	English
Access Restriction	Open
Content Type	Text
Resource Type	Article