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
Learning Component Behavior from Tests: Theory and Algorithms for Automata with Data
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
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: urn:nbn:se:uu:diva-265369ISBN: 978-91-554-9395-0 (print)OAI: oai:DiVA.org:uu-265369DiVA: diva2:865360
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
List of papers
1. Inferring Canonical Register Automata
Open this publication in new window or tab >>Inferring Canonical Register Automata
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
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7148
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-189969 (URN)10.1007/978-3-642-27940-9 (DOI)978-3-642-27939-3 (ISBN)
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
2. RALib: A LearnLib extension for inferring EFSMs
Open this publication in new window or tab >>RALib: A LearnLib extension for inferring EFSMs
2015 (English)Conference paper, Published paper (Refereed)
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-265365 (URN)
Conference
DIFTS
Available from: 2015-10-28 Created: 2015-10-28 Last updated: 2015-12-16
3. Active Learning for Extended Finite State Machines
Open this publication in new window or tab >>Active Learning for Extended Finite State Machines
2015 (English)Report (Other academic)
Series
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2015-032
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-265368 (URN)
Available from: 2015-10-28 Created: 2015-10-28 Last updated: 2015-12-16
4. A succinct canonical register automaton model
Open this publication in new window or tab >>A succinct canonical register automaton model
Show others...
2015 (English)In: Journal of Logical and Algebraic Methods in Programming, ISSN 2352-2208, Vol. 84, no 1, 54-66 p.Article in journal (Refereed) Published
Keyword
register automata, data languages, canonical model, Myhill–Nerode, automata theory
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-237501 (URN)10.1016/j.jlamp.2014.07.004 (DOI)000347601600005 ()
Conference
23rd Nordic Workshop on Programming Theory (NWPT 2011)
Projects
Connect
Available from: 2014-08-04 Created: 2014-12-03 Last updated: 2015-12-16Bibliographically approved

Open Access in DiVA

fulltext(606 kB)223 downloads
File information
File name FULLTEXT01.pdfFile size 606 kBChecksum SHA-512
b1ee878cef55bf746bf80352c8e21ccf5640f8585380dab732e2f8b6242c1ce41ea02f09b99852ec95f9ce17e839abaaf7c3b9d390ba0c8d6141e09c1bfa6adc
Type fulltextMimetype application/pdf
Buy this publication >>

By organisation
Division of Computer SystemsComputer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 223 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 2299 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