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
Regular Inference for State Machines Using Domains with Equality Tests
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.
2008 (English)In: Fundamental Approaches to Software Engineering / [ed] Fiadeiro JL; Inverardi P, Berlin: Springer-Verlag , 2008, 317-331 p.Conference paper, Published paper (Refereed)
Abstract [en]

Existing algorithms for regular inference (aka automata learning) allows to infer a finite state machine by observing the output that the machine produces in response to a selected sequence of input strings. We generalize regular inference techniques to infer a class of state machines with an infinite state space. We consider Mealy machines extended with state variables that can assume values from a potentially unbounded domain. These values can be passed as parameters in input and output symbols, and can be used in tests for equality between state variables and/or message parameters. This is to our knowledge the first extension of regular inference to infinite-state systems. We intend to use these techniques to generate models of communication protocols from observations of their input-output behavior. Such protocols often have parameters that represent node adresses, connection identifiers, etc. that have a large domain, and on which test for equality is the only meaningful operation. Our extension consists of two phases. In the first phase we apply an existing inference technique for finite-state Mealy machines to generate a model for the case that the values are taken from a small data domain. In the second phase we transform this finite-state Mealy machine into an infinite-state Mealy machine by folding it into a compact symbolic form.

Place, publisher, year, edition, pages
Berlin: Springer-Verlag , 2008. 317-331 p.
Series
Lecture Notes in Computer Science, 4961
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-98085DOI: 10.1007/978-3-540-78743-3_24ISI: 000254603000024ISBN: 978-3-540-78742-6 (print)OAI: oai:DiVA.org:uu-98085DiVA: diva2:173261
Conference
11th International Conference on Fundamental Approaches to Software Engineering Budapest, HUNGARY, MAR 29-APR 06, 2008
Available from: 2009-02-06 Created: 2009-02-06 Last updated: 2011-03-24Bibliographically approved
In thesis
1. Regular Inference for Communication Protocol Entities
Open this publication in new window or tab >>Regular Inference for Communication Protocol Entities
2009 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

A way to create well-functioning computer systems is to automate error detection in the systems. Automated techniques for finding errors, such as testing and formal verification, requires a model of the system. The technique for constructing deterministic finite automata (DFA) models, without access to the source code, is called regular inference. The technique provides sequences of input, so called membership queries, to a system, observes the responses, and infers a model from the input and responses.

This thesis presents work to adapt regular inference to a certain kind of systems: communication protocol entities. Such entities interact by sending and receiving messages consisting of a message type and a number of parameters, each of which potentially can take on a large number of values. This may cause a model of a communication protocol entity inferred by regular inference, to be very large and take a long time to infer. Since regular inference creates a model from the observed behavior of a communication protocol entity, the model may be very different from a designer's model of the system's source code.

This thesis presents adaptations of regular inference to infer more compact models and use less membership queries. The first contribution is a survey over three algorithms for regular inference. We present their similarities and their differences in terms of the required number of membership queries. The second contribution is an investigation on how many membership queries a common regular inference algorithm, the L* algorithm by Angluin, requires for randomly generated DFAs and randomly generated DFAs with a structure common for communication protocol entities. In comparison, the DFAs with a structure common for communication protocol entities require more membership queries. The third contribution is an adaptation of regular inference to communication protocol entities which behavior foremost are affected by the message types. The adapted algorithm avoids asking membership queries containing messages with parameter values that results in already observed responses. The fourth contribution is an approach for regular inference of communication protocol entities which communicate with messages containing parameter values from very large ranges. The approach infers compact models, and uses parameter values taken from a small portion of their ranges in membership queries. The fifth contribution is an approach to infer compact models of communication protocol entities which have a similar partitioning of an entity's behavior into control states as in a designer's model of the protocol.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2009. 66 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 605
National Category
Computer Engineering
Identifiers
urn:nbn:se:uu:diva-9559 (URN)978-91-554-7420-1 (ISBN)
Public defence
2009-03-19, Room 2446, Polacksbacken, Lägerhyddsvägen 2D, Uppsala, 10:00 (English)
Opponent
Supervisors
Available from: 2009-02-25 Created: 2009-02-06 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Berg, ThereseJonsson, Bengt

Search in DiVA

By author/editor
Berg, ThereseJonsson, Bengt
By organisation
Computer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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