Test Generation Derived from Model-Checking

Model-checking and testing are different activities, at least conceptually. While model-checking consists in comparing two specifications at different abstraction levels, testing consists in trying to find errors or gain some confidence in the correctness of an implementation with respect to a specification by the execution of test cases. Nevertheless, there are also similarities in models and algorithms. We argue for this by giving a new on-the-fly test generation algorithm which is an adaptation of a classical graph algorithm which also serves as a basis of some model-checking algorithms. This algorithm is the Tarjan’s algorithm which computes the strongly connected components of a digraph.