B Model Slicing and Predicate Abstraction to Generate Tests - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Software Quality Journal Année : 2011

B Model Slicing and Predicate Abstraction to Generate Tests

Résumé

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.
Fichier principal
Vignette du fichier
sqj-jsbm.pdf (347.44 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00650661 , version 1 (12-12-2011)

Identifiants

Citer

Jacques Julliand, Nicolas Stouls, Pierre-Christophe Bué, Pierre-Alain Masson. B Model Slicing and Predicate Abstraction to Generate Tests. Software Quality Journal, 2011, pp.1-32. ⟨10.1007/s11219-011-9161-8⟩. ⟨hal-00650661⟩
228 Consultations
248 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More