Test Generation from Event System Abstractions to Cover Their States and Transitions

Abstract

Model-based testing of event systems can take advantage of considering abstractions rather than explicit models, for controlling their size. When abstracting still a test has to be a concrete connected and reachable event sequence. This paper presents a test generation method based on computing a reachable and connected under-approximation of the abstraction of an event system. We compute the under-approximation with concrete instances of the abstract transitions, that cover all the states and transitions of the predicatebased abstraction. We propose an algorithmic method that instantiates each of the abstract transitions, and maintains for widening it a frontier of concretely reached states. We present heuristics to favour the instances connectivity. The idea is to prolong whenever possible the already reached sequences of concrete transitions, and to parameterize the order in which the states and actions occur. This concrete under-approximation ends up covering partially (at best totally) the reachable abstract transitions. The computed tests are paths of the under-approximation. The paper also reports on an implementation, which permits to provide experimental results confirming the interest of the approach with related heuristics.