Using Invariant Detection Mechanism in Black Box Inference
Résumé
The testing and formal verification of black box software components
is a challenging domain. The problem is even harder when specifications of
these components are not available. An approach to cope with this problem
is to combine testing with learning techniques, such that the learned models
of the components can be used to explore unknown implementation and thus
facilitate testing efforts. In recent years, we have contributed to this approach by
proposing techniques for learning parameterized state machine models and then
use them in the integration testing of black box components. The major problem
in this technique left unaddressed was the selection of parameter values during
the learning process. In this paper, we propose to use an invariant detection
mechanism to select values in the learning process, thus refining model inference
and testing approach. Initial experiments with small examples yielded positive
results.