Tri-modal under-approximation of event systems 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 models. This allows a model-based testing approach to operate on an abstraction of 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. We propose as a solution to this problem to symbolically explore the set of states reachable after a finite number of steps, to identify the Ball chains that start in any of these states. 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. Finally we show by means of preliminary experimental results that, despite the complexity of symbolic exploration, the method is able to reach many Ball chains within a small number of exploration steps.