Automata Learning through Counterexample Guided Abstraction Refinement

Fides Aarts, Faranak Heidarian, Harco Kuppens, Petur Olsen, Frits Vaandrager

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

32 Citationer (Scopus)

Resumé

Abstraction is the key when learning behavioral models of realistic systems. Hence, in most practical applications where automata learning is used to construct models of software components, researchers manually define abstractions which, depending on the history, map a large set of concrete events to a small set of abstract events that can be handled by automata learning tools. In this article, we show how such abstractions can be constructed fully automatically for a restricted class of extended finite state machines in which one can test for equality of data parameters, but no operations on data are allowed. Our approach uses counterexample-guided abstraction refinement: whenever the current abstraction is too coarse and induces nondeterministic behavior, the abstraction is refined automatically. Using Tomte, a prototype tool implementing our algorithm, we have succeeded to learn – fully automatically – models of several realistic software components, including the biometric passport and the SIP protocol.
OriginalsprogEngelsk
TitelFM 2012: Formal Methods : 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings
Antal sider18
Vol/bind7436
ForlagSpringer
Publikationsdato2012
Sider10-27
ISBN (Trykt)978-3-642-32758-2
ISBN (Elektronisk)978-3-642-32759-9
DOI
StatusUdgivet - 2012
BegivenhedFormal Methods 2012: 18th International Symposium on Formal Mehtods - CNAM, Paris, Frankrig
Varighed: 27 aug. 201231 aug. 2012
Konferencens nummer: 18

Konference

KonferenceFormal Methods 2012
Nummer18
LokationCNAM
LandFrankrig
ByParis
Periode27/08/201231/08/2012
NavnLecture Notes in Computer Science
Vol/bind7436
ISSN0302-9743

Fingerprint

Finite automata
Biometrics
Concretes
Network protocols

Citer dette

Aarts, F., Heidarian, F., Kuppens, H., Olsen, P., & Vaandrager, F. (2012). Automata Learning through Counterexample Guided Abstraction Refinement. I FM 2012: Formal Methods : 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings (Bind 7436, s. 10-27). Springer. Lecture Notes in Computer Science, Bind. 7436 https://doi.org/10.1007/978-3-642-32759-9_4
Aarts, Fides ; Heidarian, Faranak ; Kuppens, Harco ; Olsen, Petur ; Vaandrager, Frits. / Automata Learning through Counterexample Guided Abstraction Refinement. FM 2012: Formal Methods : 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. Bind 7436 Springer, 2012. s. 10-27 (Lecture Notes in Computer Science, Bind 7436).
@inproceedings{e3460d3839bd4ba6956a67e840acceec,
title = "Automata Learning through Counterexample Guided Abstraction Refinement",
abstract = "Abstraction is the key when learning behavioral models of realistic systems. Hence, in most practical applications where automata learning is used to construct models of software components, researchers manually define abstractions which, depending on the history, map a large set of concrete events to a small set of abstract events that can be handled by automata learning tools. In this article, we show how such abstractions can be constructed fully automatically for a restricted class of extended finite state machines in which one can test for equality of data parameters, but no operations on data are allowed. Our approach uses counterexample-guided abstraction refinement: whenever the current abstraction is too coarse and induces nondeterministic behavior, the abstraction is refined automatically. Using Tomte, a prototype tool implementing our algorithm, we have succeeded to learn – fully automatically – models of several realistic software components, including the biometric passport and the SIP protocol.",
author = "Fides Aarts and Faranak Heidarian and Harco Kuppens and Petur Olsen and Frits Vaandrager",
year = "2012",
doi = "10.1007/978-3-642-32759-9_4",
language = "English",
isbn = "978-3-642-32758-2",
volume = "7436",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "10--27",
booktitle = "FM 2012: Formal Methods",
address = "Germany",

}

Aarts, F, Heidarian, F, Kuppens, H, Olsen, P & Vaandrager, F 2012, Automata Learning through Counterexample Guided Abstraction Refinement. i FM 2012: Formal Methods : 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. bind 7436, Springer, Lecture Notes in Computer Science, bind 7436, s. 10-27, Formal Methods 2012, Paris, Frankrig, 27/08/2012. https://doi.org/10.1007/978-3-642-32759-9_4

Automata Learning through Counterexample Guided Abstraction Refinement. / Aarts, Fides; Heidarian, Faranak; Kuppens, Harco; Olsen, Petur; Vaandrager, Frits.

FM 2012: Formal Methods : 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. Bind 7436 Springer, 2012. s. 10-27 (Lecture Notes in Computer Science, Bind 7436).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - Automata Learning through Counterexample Guided Abstraction Refinement

AU - Aarts, Fides

AU - Heidarian, Faranak

AU - Kuppens, Harco

AU - Olsen, Petur

AU - Vaandrager, Frits

PY - 2012

Y1 - 2012

N2 - Abstraction is the key when learning behavioral models of realistic systems. Hence, in most practical applications where automata learning is used to construct models of software components, researchers manually define abstractions which, depending on the history, map a large set of concrete events to a small set of abstract events that can be handled by automata learning tools. In this article, we show how such abstractions can be constructed fully automatically for a restricted class of extended finite state machines in which one can test for equality of data parameters, but no operations on data are allowed. Our approach uses counterexample-guided abstraction refinement: whenever the current abstraction is too coarse and induces nondeterministic behavior, the abstraction is refined automatically. Using Tomte, a prototype tool implementing our algorithm, we have succeeded to learn – fully automatically – models of several realistic software components, including the biometric passport and the SIP protocol.

AB - Abstraction is the key when learning behavioral models of realistic systems. Hence, in most practical applications where automata learning is used to construct models of software components, researchers manually define abstractions which, depending on the history, map a large set of concrete events to a small set of abstract events that can be handled by automata learning tools. In this article, we show how such abstractions can be constructed fully automatically for a restricted class of extended finite state machines in which one can test for equality of data parameters, but no operations on data are allowed. Our approach uses counterexample-guided abstraction refinement: whenever the current abstraction is too coarse and induces nondeterministic behavior, the abstraction is refined automatically. Using Tomte, a prototype tool implementing our algorithm, we have succeeded to learn – fully automatically – models of several realistic software components, including the biometric passport and the SIP protocol.

UR - http://www.scopus.com/inward/record.url?scp=84866000299&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-32759-9_4

DO - 10.1007/978-3-642-32759-9_4

M3 - Article in proceeding

SN - 978-3-642-32758-2

VL - 7436

T3 - Lecture Notes in Computer Science

SP - 10

EP - 27

BT - FM 2012: Formal Methods

PB - Springer

ER -

Aarts F, Heidarian F, Kuppens H, Olsen P, Vaandrager F. Automata Learning through Counterexample Guided Abstraction Refinement. I FM 2012: Formal Methods : 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. Bind 7436. Springer. 2012. s. 10-27. (Lecture Notes in Computer Science, Bind 7436). https://doi.org/10.1007/978-3-642-32759-9_4