B Model Slicing and Predicate Abstraction to Generate Tests

Abstract : In a model-based testing approach as well as for the verification of properties, B models provide an interesting modeling solution. However, for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used. The abstraction is often a domain abstraction of the state variables that requires many proof obligations to be discharged, which can be very time-consuming for real applications. This paper presents a contribution to this problem that complements an approach based on domain abstraction for test generation, by adding a preliminary syntactic abstraction phase, based on variable elimination. We define a syntactic transformation that suppresses some variables from a B event model, in addition to three methods that choose relevant variables according to a test purpose. In this way, we propose a method that computes an abstraction of a source model {\mathsf{M}} according to a set of selected relevant variables. Depending on the method used, the abstraction can be computed as a simulation or as a bisimulation of {\mathsf{M}}. With this approach, the abstraction process produces a finite state system. We apply this abstraction computation to a model-based testing process. We evaluate experimentally the impact of the model simplification by variables' elimination on the size of the models, on the number of proof obligations to discharge, on the precision of the abstraction and on the coverage achieved by the test generation.
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00650661
Contributeur : Nicolas Stouls <>
Soumis le : lundi 12 décembre 2011 - 08:09:56
Dernière modification le : mercredi 29 novembre 2017 - 16:17:45
Document(s) archivé(s) le : mardi 13 mars 2012 - 02:21:33

Fichier

sqj-jsbm.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Jacques Julliand, Nicolas Stouls, Pierre-Christophe Bué, Pierre-Alain Masson. B Model Slicing and Predicate Abstraction to Generate Tests. Software Quality Journal, Springer Verlag, 2011, pp.1-32. 〈http://www.springerlink.com/content/920k72185701j61m/〉. 〈10.1007/s11219-011-9161-8〉. 〈hal-00650661〉

Partager

Métriques

Consultations de la notice

300

Téléchargements de fichiers

188