Sound black-box checking in the LearnLib

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Standard

Sound black-box checking in the LearnLib. / Meijer, Jeroen; van de Pol, Jaco.

In: Innovations in Systems and Software Engineering, Vol. 15, No. 3-4, 09.2019, p. 267-287.

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Harvard

Meijer, J & van de Pol, J 2019, 'Sound black-box checking in the LearnLib', Innovations in Systems and Software Engineering, vol. 15, no. 3-4, pp. 267-287. https://doi.org/10.1007/s11334-019-00342-6

APA

Meijer, J., & van de Pol, J. (2019). Sound black-box checking in the LearnLib. Innovations in Systems and Software Engineering, 15(3-4), 267-287. https://doi.org/10.1007/s11334-019-00342-6

CBE

Meijer J, van de Pol J. 2019. Sound black-box checking in the LearnLib. Innovations in Systems and Software Engineering. 15(3-4):267-287. https://doi.org/10.1007/s11334-019-00342-6

MLA

Meijer, Jeroen and Jaco van de Pol. "Sound black-box checking in the LearnLib". Innovations in Systems and Software Engineering. 2019, 15(3-4). 267-287. https://doi.org/10.1007/s11334-019-00342-6

Vancouver

Meijer J, van de Pol J. Sound black-box checking in the LearnLib. Innovations in Systems and Software Engineering. 2019 Sep;15(3-4):267-287. https://doi.org/10.1007/s11334-019-00342-6

Author

Meijer, Jeroen ; van de Pol, Jaco. / Sound black-box checking in the LearnLib. In: Innovations in Systems and Software Engineering. 2019 ; Vol. 15, No. 3-4. pp. 267-287.

Bibtex

@article{55be6c9c38fe42c6b51bce1155559bd1,
title = "Sound black-box checking in the LearnLib",
abstract = "In black-box checking (BBC) incremental hypotheses on the behavior of a system are learned in the form of finite automata, using information from a given set of requirements, specified in Linear-time Temporal Logic (LTL). The LTL formulae are checked on intermediate automata and potential counterexamples are validated on the actual system. Spurious counterexamples are used by the learner to refine these automata. We improve BBC in two directions. First, we improve checking lasso-like counterexamples by assuming a check for state equivalence. This provides a sound method without knowing an upper-bound on the number of states in the system. Second, we propose to check the safety portion of an LTL property first, by deriving simple counterexamples using monitors. We extended LearnLib{\textquoteright}s system under learning API to make our methods accessible, using LTSmin as model checker under the hood. We illustrate how LearnLib{\textquoteright}s most recent active learning algorithms can be used for BBC in practice. Using the RERS 2017 challenge, we provide experimental results on the performance of all LearnLib{\textquoteright}s active learning algorithms when applied in a BBC setting. We will show that the novel incremental algorithms TTT and ADT perform the best. We also provide experiments on the efficiency of various BBC strategies.",
keywords = "Black-box checking, B{\"u}chi automata, Learn-based testing, LearnLib, LTL, LTSmin, Model checking, Monitors",
author = "Jeroen Meijer and {van de Pol}, Jaco",
year = "2019",
month = sep,
doi = "10.1007/s11334-019-00342-6",
language = "English",
volume = "15",
pages = "267--287",
journal = "Innovations in Systems and Software Engineering",
issn = "1614-5046",
publisher = "Springer U K",
number = "3-4",

}

RIS

TY - JOUR

T1 - Sound black-box checking in the LearnLib

AU - Meijer, Jeroen

AU - van de Pol, Jaco

PY - 2019/9

Y1 - 2019/9

N2 - In black-box checking (BBC) incremental hypotheses on the behavior of a system are learned in the form of finite automata, using information from a given set of requirements, specified in Linear-time Temporal Logic (LTL). The LTL formulae are checked on intermediate automata and potential counterexamples are validated on the actual system. Spurious counterexamples are used by the learner to refine these automata. We improve BBC in two directions. First, we improve checking lasso-like counterexamples by assuming a check for state equivalence. This provides a sound method without knowing an upper-bound on the number of states in the system. Second, we propose to check the safety portion of an LTL property first, by deriving simple counterexamples using monitors. We extended LearnLib’s system under learning API to make our methods accessible, using LTSmin as model checker under the hood. We illustrate how LearnLib’s most recent active learning algorithms can be used for BBC in practice. Using the RERS 2017 challenge, we provide experimental results on the performance of all LearnLib’s active learning algorithms when applied in a BBC setting. We will show that the novel incremental algorithms TTT and ADT perform the best. We also provide experiments on the efficiency of various BBC strategies.

AB - In black-box checking (BBC) incremental hypotheses on the behavior of a system are learned in the form of finite automata, using information from a given set of requirements, specified in Linear-time Temporal Logic (LTL). The LTL formulae are checked on intermediate automata and potential counterexamples are validated on the actual system. Spurious counterexamples are used by the learner to refine these automata. We improve BBC in two directions. First, we improve checking lasso-like counterexamples by assuming a check for state equivalence. This provides a sound method without knowing an upper-bound on the number of states in the system. Second, we propose to check the safety portion of an LTL property first, by deriving simple counterexamples using monitors. We extended LearnLib’s system under learning API to make our methods accessible, using LTSmin as model checker under the hood. We illustrate how LearnLib’s most recent active learning algorithms can be used for BBC in practice. Using the RERS 2017 challenge, we provide experimental results on the performance of all LearnLib’s active learning algorithms when applied in a BBC setting. We will show that the novel incremental algorithms TTT and ADT perform the best. We also provide experiments on the efficiency of various BBC strategies.

KW - Black-box checking

KW - Büchi automata

KW - Learn-based testing

KW - LearnLib

KW - LTL

KW - LTSmin

KW - Model checking

KW - Monitors

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

U2 - 10.1007/s11334-019-00342-6

DO - 10.1007/s11334-019-00342-6

M3 - Journal article

AN - SCOPUS:85066607750

VL - 15

SP - 267

EP - 287

JO - Innovations in Systems and Software Engineering

JF - Innovations in Systems and Software Engineering

SN - 1614-5046

IS - 3-4

ER -