Sound Black-Box Checking in the LearnLib

Jeroen Meijer, Jaco van de Pol

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)
    188 Downloads (Pure)

    Abstract

    In Black-Box Checking (BBC) incremental hypotheses of a system are learned in the form of finite automata. On these automata LTL formulae are verified, or their counterexamples validated on the actual system. We extend the LearnLib’s system-under-learning API for sound BBC, by means of state equivalence, that contrasts the original proposal where an upper-bound on the number of states in the system is assumed. We will show how LearnLib’s new BBC algorithms can be used in practice, as well as how one could experiment with different model checkers and BBC algorithms. 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. The performance of learning algorithms was unknown for this setting. We will show that the novel incremental algorithms TTT, and ADT perform the best.
    Original languageEnglish
    Title of host publicationNASA Formal Methods
    Subtitle of host publication10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings
    EditorsAaron Dutle, César A. Muñoz, Anthony Narkawicz
    Place of PublicationCham
    PublisherSpringer
    Pages349-366
    Number of pages18
    ISBN (Electronic)978-3-319-77935-5
    ISBN (Print)978-3-319-77934-8
    DOIs
    Publication statusPublished - 11 Mar 2018

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume10811
    ISSN (Print)0302-9743

    Fingerprint Dive into the research topics of 'Sound Black-Box Checking in the LearnLib'. Together they form a unique fingerprint.

    Cite this