Under-Approximation Generation Driven by Relevance Predicates and Variants

In test generation, when computing a reachable concrete under-approximation of an event system's predicate abstraction, we aim at covering each reachable abstract transition with at least one reachable concrete instance. As this is in general undecidable, an algorithm must finitely instantiate the abstract transitions for it to terminate. The approach defended in this paper is to first concretely explore the abstract graph, while concretizing the abstract transitions met at most once. However, some abstract transitions would require that loops were taken previously for them to become reached. To this end, in a second phase, a test engineer guides the exploration by describing a relevance predicate able to travel such loops. We give hints on how to design and express a relevance predicate, and provide a method for automatically extracting a variant out of it. A relevance guided concretization algorithm is given, whose termination is ensured by using this variant. Experimental results are provided that show the interest of the approach.