In this paper, we review behavior-based model construction from a point of view characterized by
verification, model checking, and
abstraction. It turns out that
abstract interpretation is the key to scaling known learning techniques for practical applications, that
model checking may serve as a teaching aid in the learning process underlying the model construction, and that there are various synergies with other validation and
verification techniques. We will illustrate our discussion by means of a realistic telecommunications scenario, where the underlying system has grown over the last two decades, the available system documentation consists of not much more than user manuals and protocol standards, and the revision cycle times are extremely short. In this situation, behavior-based model construction provides a sound basis, e.g., for test-suite design and maintenance, test organization, and test evaluation.
Keywords Automata learning - Model checking - Abstraction - Testing