Active learning of nondeterministic systems from an ioco perspective
conference paper
Model-based testing allows the creation of test cases from a model of the system under test. Often, such models are difficult to obtain, or even not available. Automata learning helps in inferring the model of a system by observing its behaviour. The model can be employed for many purposes, such as testing other implementations, regression testing, or model checking. We present an algorithm for active learning of nondeterministic, input-enabled, labelled transition systems, based on the well known Angluin’s L* algorithm. Under some assumptions, for dealing with nondeterminism, input-enabledness and equivalence checking, we prove that the algorithm produces a model whose behaviour is equivalent to the one under learning. We define new properties for the structure used in the algorithm, derived from the semantics of labelled transition systems. Such properties help the learning, by avoiding to query the system under learning when it is not necessary.
Topics
TNO Identifier
520156
ISSN
03029743
ISBN
9783662452332
Publisher
Springer Verlag
Source title
6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2014; Imperial, Corfu; Greece; 8 October 2014 through 11 October 2014
Editor(s)
Margaria T.
Steffen B.
Margaria T.
Steffen B.
Margaria T.
Pages
220-235
Files
To receive the publication files, please send an e-mail request to TNO Repository.