uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Inferring Canonical Register Automata
Technical University of Dortmund.
Technical University of Dortmund.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2012 (English)In: Verification, Model Checking, and Abstract Interpretation - 13th International Conference, / [ed] Viktor Kuncak and Andrey Rybalchenko, Springer, 2012, 251-266 p.Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we present an extension of active automata learning to register automata, an automaton model which is capable of expressing the influence of data on control flow. Register automata operate on an infinite data domain, whose values can be assigned to registers and compared for equality. Our active learning algorithm is unique in that it directly infers the effect of data values on control flow as part of the learning process. This effect is expressed by means of registers and guarded transitions in the resulting register automata models. The application of our algorithm to a small example indicates the impact of learning register automata models: Not only are the inferred models much more expressive than finite state machines, but the prototype implementation also drastically outperforms the classic L* algorithm, even when exploiting optimal data abstraction and symmetry reduction.

Place, publisher, year, edition, pages
Springer, 2012. 251-266 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7148
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-189969DOI: 10.1007/978-3-642-27940-9ISBN: 978-3-642-27939-3 (print)OAI: oai:DiVA.org:uu-189969DiVA: diva2:582621
Conference
VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012.
Projects
ConnectUPMARC
Available from: 2013-01-05 Created: 2013-01-05 Last updated: 2015-11-26
In thesis
1. Learning Component Behavior from Tests: Theory and Algorithms for Automata with Data
Open this publication in new window or tab >>Learning Component Behavior from Tests: Theory and Algorithms for Automata with Data
2015 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Formal models are often used to describe the behavior of a computer program or component. Behavioral models have many different usages, e.g., in model-based techniques for software development and verification,such as model checking and model based testing.

The application of model-based techniques is hampered by the current lack of adequate models for most actual systems, largely due to the significant manual effort typically needed to construct them. To remedy this, automata learning techniques (whereby models can be inferred by performing tests on a component) have been developed for finite automata that capture control flow. However, many usages requiremodels also to capture data flow, i.e., how behavior is affected by data values in method invocations and commands. Unfortunately, techniques are less developed for models that combinecontrol flow with data.

In this thesis, we extend automata learning to infer automata models that captureboth control flow and data flow. We base our technique on a corresponding extension of classical automata theoryto capture data.

We define a formalism for register automata, a model that extends finite automata by adding registers that can store data values and be used in guards and assignments on transitions. Our formalism is parameterized on a theory, i.e., a set of relations on a data domain. We present a Nerode congruence for the languages that our register automata can recognize, and provide a Myhill-Nerode theorem for constructing canonical register automata, thereby extending classical automata theory to register automata.

We also present a learning algorithm for register automata: the new SL* algorithm, which extends the well-known L* algorithm for finite automata. The SL* algorithm is based on our new Nerode congruence, and uses a novel technique to infer symbolic data constraints on parameters. We evaluated our algorithm in a black-box scenario, inferring, e.g., the connection establishment phase of TCP and a priority queue, in addition to a number of smaller models. The SL* algorithm is implemented in a tool, which allows for use in more realistic settings, e.g., where models have both input and output, and for directly inferring Java classes.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2015. 70 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1311
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-265369 (URN)978-91-554-9395-0 (ISBN)
Public defence
2015-12-17, ITC 2446, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
Opponent
Supervisors
Available from: 2015-11-26 Created: 2015-10-28 Last updated: 2016-01-13

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Jonsson, Bengt

Search in DiVA

By author/editor
Jonsson, Bengt
By organisation
Computer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 446 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf