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

Contributeur : Nicolas Stouls <>
Soumis le : lundi 12 décembre 2011 - 08:09:56
Dernière modification le : mercredi 28 novembre 2018 - 09:36:02
Document(s) archivé(s) le : mardi 13 mars 2012 - 02:21:33


Fichiers produits par l'(les) auteur(s)



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〉



Consultations de la notice


Téléchargements de fichiers