Publication Date:
2015-05-03
Description:
We propose an approach which, given a state-transition model of a system, constructs, in parallel, an approximate automaton model and a test suite for the system. The approximate model construction relies on a variant of Angluin's automata learning algorithm, adapted to finite cover automata. A finite cover automaton represents an approximation of the system that only considers sequences of length up to an established upper bound . Crucially, the size of the cover automaton, which normally depends on , can be significantly lower than the size of the exact automaton model. Thus, controlling , the state explosion problem normally associated with constructing and checking state-based models can be mitigated. The proposed approach also allows for a gradual construction of the model and of the associated test suite, with complexity and time savings. Moreover, we provide automation of counterexample search, by a combination of black-box and random testing, and metrics to evaluate the quality of the produced results. The approach is presented and implemented in the context of the Event-B modeling language, but its underlying ideas and principles are much more general and can be applied to any system whose behavior can be suitably described by a state-transition model.
Print ISSN:
0010-4620
Electronic ISSN:
1460-2067
Topics:
Computer Science
