Tri-modal under-approximation for test generation

This paper presents a method for under-approximating behavioural models with the guarantee that the abstract paths can be instantiated as executions of the models. This allows a model-based testing approach to operate on an abstraction of an infinite or very large behavioural model. We characterize the abstract transitions as may, must+ or must-. This allows us to benefit from Thomas Ball's result that any abstract sequence in the shape of must-*.may.must+* (a Ball chain) can be instantiated as a sequence of connected concrete transitions. We adapt Ball's work aiming at abstracting C programs to the case of event systems, where the instantiated Ball chains might not be reachable from a model's initial state because our method can abstract the control structure. We propose as a solution to this problem to symbolically explore the set of states reachable after a finite number of steps. The Ball chains that start in any of these states are reachable and instantiable. By keeping track of the paths that lead to these starting states, we are able to instantiate with certainty the sequences made of the reached Ball chains with their prefix. This method improves the usual methods that often look for instantiations even though they don't exist for some sequences. We also propose in this paper a way to compute the abstraction w.r.t. predicates that are automatically extracted out of a dynamic property expressed in the Dwyer et al. language. We give experimental results obtained via a proof-of-concept prototype that we have implemented. They show that many Ball chains are exhibited, reached and concretized by our method, and that despite the complexity of symbolic exploration, the Ball chains can be reached within a small number of exploration steps.