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

Direct link
Generating models of infinite-state communication protocols using regular inference with abstraction
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2015 (English)In: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 46, no 1, 1-41 p.Article in journal (Refereed) Published
Abstract [en]

In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular inference techniques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant impact on control flow in many communication protocols. We present a framework, which adapts regular inference to include data parameters in messages and states for generating components with large or infinite message alphabets. A main idea is to adapt the framework of predicate abstraction, successfully used in formal verification. Since we are in a black-box setting, the abstraction must be supplied externally, using information about how the component manages data parameters. We have implemented our techniques by connecting the LearnLib tool for regular inference with an implementation of session initiation protocol (SIP) in ns-2 and an implementation of transmission control protocol (TCP) in Windows 8, and generated models of SIP and TCP components.

Place, publisher, year, edition, pages
2015. Vol. 46, no 1, 1-41 p.
National Category
Computer Systems
URN: urn:nbn:se:uu:diva-238141DOI: 10.1007/s10703-014-0216-xISI: 000352157500001OAI: oai:DiVA.org:uu-238141DiVA: diva2:770107
Available from: 2014-11-19 Created: 2014-12-09 Last updated: 2015-12-16Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Jonsson, Bengt
By organisation
Computer Systems
In the same journal
Formal methods in system design
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
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

Altmetric score

Total: 671 hits
ReferencesLink to record
Permanent link

Direct link