Skip to Main content Skip to Navigation
New interface
Journal articles

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.
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Nicolas Stouls Connect in order to contact the contributor
Submitted on : Monday, December 12, 2011 - 8:09:56 AM
Last modification on : Monday, July 18, 2022 - 1:46:36 PM
Long-term archiving on: : Tuesday, March 13, 2012 - 2:21:33 AM


Files produced by the author(s)



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⟩



Record views


Files downloads