Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
Medientyp:
E-Artikel
Titel:
Active learning for extended finite state machines
Beteiligte:
Cassel, Sofia;
Howar, Falk;
Jonsson, Bengt;
Steffen, Bernhard
Erschienen:
Association for Computing Machinery (ACM), 2016
Erschienen in:
Formal Aspects of Computing, 28 (2016) 2, Seite 233-263
Sprache:
Englisch
DOI:
10.1007/s00165-016-0355-5
ISSN:
0934-5043;
1433-299X
Entstehung:
Anmerkungen:
Beschreibung:
<jats:title>Abstract</jats:title>
<jats:p>
We present a black-box active learning algorithm for inferring extended finite state machines (EFSM)s by dynamic black-box analysis. EFSMs can be used to model both data flow and control behavior of software and hardware components. Different dialects of EFSMs are widely used in tools for model-based software development, verification, and testing. Our algorithm infers a class of EFSMs called
<jats:italic>register automata</jats:italic>
. Register automata have a finite control structure, extended with variables (registers), assignments, and guards. Our algorithm is parameterized on a particular
<jats:italic>theory</jats:italic>
, i.e., a set of operations and tests on the data domain that can be used in guards.
</jats:p>
<jats:p>
Key to our learning technique is a novel learning model based on so-called
<jats:italic>tree queries</jats:italic>
. The learning algorithm uses tree queries to infer symbolic data constraints on parameters, e.g., sequence numbers, time stamps, identifiers, or even simple arithmetic. We describe sufficient conditions for the properties that the symbolic constraints provided by a tree query in general must have to be usable in our learning model. We also show that, under these conditions, our framework induces a generalization of the classical Nerode equivalence and canonical automata construction to the symbolic setting. We have evaluated our algorithm in a black-box scenario, where tree queries are realized through (black-box) testing. Our case studies include connection establishment in TCP and a priority queue from the Java Class Library.
</jats:p>