Automata Learning through Counterexample Guided Abstraction Refinement
| Autor: | Aarts, Fides, Heidarian, F., Kuppens, H., Olsen, P., Vaandrager, F., Giannakopoulou, D. |
|---|---|
| Přispěvatelé: | Giannakopoulou, D. |
| Rok vydání: | 2012 |
| Předmět: |
Class (computer programming)
Finite-state machine Programming language business.industry Computer science Construct (python library) computer.software_genre Nondeterministic algorithm Component-based software engineering Software Science Key (cryptography) Lecture Notes in Computer Science Abstraction Artificial intelligence business computer Counterexample |
| Zdroj: | FM 2012: Formal Methods ISBN: 9783642327582 FM Giannakopoulou, D. (ed.), FM 2012 : Formal Methods :18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, pp. 10-27 Lecture Notes in Computer Science ; 7436, 10-27. Berlin : Springer STARTPAGE=10;ENDPAGE=27;TITLE=Lecture Notes in Computer Science ; 7436 |
| DOI: | 10.1007/978-3-642-32759-9_4 |
| Popis: | ion 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|