Efficient learning and analysis of system behavior

Jeroen Meijer

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    108 Downloads (Pure)

    Abstract

    In this thesis, we present techniques for more efficient learning and analysis of system behavior.

    The first part covers novel algorithms and tooling for testing systems based on active automata learning and Linear-time Temporal Logic (LTL) model checking, also called Learning-Based Testing (LBT). Next, we provide an improved learning algorithm that is able to deal with huge alphabets. These are commonly seen in large-scale industrial systems where input symbols contain data parameters.

    In the second part we discuss improvements for analyzing formal system specifications. We start out by looking at separated read, write and copy dependencies for symbolic model checking to speed up the verification of these specifications. Then, we show that bandwidth reduction techniques, originally designed for sparse matrix solvers, are very capable at reducing the memory footprint of the specifications' symbolic state space. Implementations of the presented algorithms are subjected to case studies and rigorous experimentation with scientific software competitions.
    Original languageEnglish
    QualificationDoctor of Philosophy
    Awarding Institution
    • University of Twente
    Supervisors/Advisors
    • van de Pol, Jaco , Supervisor
    • Stoelinga, Mariëlle Ida Antoinette, Supervisor
    Award date20 Sep 2019
    Place of PublicationEnschede
    Publisher
    Print ISBNs978-90-365-4844-1
    DOIs
    Publication statusPublished - 20 Sep 2019

    Fingerprint

    Model checking
    Specifications
    Temporal logic
    Testing
    Learning algorithms
    Bandwidth
    Data storage equipment

    Cite this

    Meijer, Jeroen. / Efficient learning and analysis of system behavior. Enschede : University of Twente, 2019. 201 p.
    @phdthesis{f238a2b1479a4b35be666de261c96c0a,
    title = "Efficient learning and analysis of system behavior",
    abstract = "In this thesis, we present techniques for more efficient learning and analysis of system behavior. The first part covers novel algorithms and tooling for testing systems based on active automata learning and Linear-time Temporal Logic (LTL) model checking, also called Learning-Based Testing (LBT). Next, we provide an improved learning algorithm that is able to deal with huge alphabets. These are commonly seen in large-scale industrial systems where input symbols contain data parameters.In the second part we discuss improvements for analyzing formal system specifications. We start out by looking at separated read, write and copy dependencies for symbolic model checking to speed up the verification of these specifications. Then, we show that bandwidth reduction techniques, originally designed for sparse matrix solvers, are very capable at reducing the memory footprint of the specifications' symbolic state space. Implementations of the presented algorithms are subjected to case studies and rigorous experimentation with scientific software competitions.",
    author = "Jeroen Meijer",
    year = "2019",
    month = "9",
    day = "20",
    doi = "10.3990/1.9789036548441",
    language = "English",
    isbn = "978-90-365-4844-1",
    series = "DSI Ph.D. thesis series",
    publisher = "University of Twente",
    number = "19-015",
    address = "Netherlands",
    school = "University of Twente",

    }

    Meijer, J 2019, 'Efficient learning and analysis of system behavior', Doctor of Philosophy, University of Twente, Enschede. https://doi.org/10.3990/1.9789036548441

    Efficient learning and analysis of system behavior. / Meijer, Jeroen.

    Enschede : University of Twente, 2019. 201 p.

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    TY - THES

    T1 - Efficient learning and analysis of system behavior

    AU - Meijer, Jeroen

    PY - 2019/9/20

    Y1 - 2019/9/20

    N2 - In this thesis, we present techniques for more efficient learning and analysis of system behavior. The first part covers novel algorithms and tooling for testing systems based on active automata learning and Linear-time Temporal Logic (LTL) model checking, also called Learning-Based Testing (LBT). Next, we provide an improved learning algorithm that is able to deal with huge alphabets. These are commonly seen in large-scale industrial systems where input symbols contain data parameters.In the second part we discuss improvements for analyzing formal system specifications. We start out by looking at separated read, write and copy dependencies for symbolic model checking to speed up the verification of these specifications. Then, we show that bandwidth reduction techniques, originally designed for sparse matrix solvers, are very capable at reducing the memory footprint of the specifications' symbolic state space. Implementations of the presented algorithms are subjected to case studies and rigorous experimentation with scientific software competitions.

    AB - In this thesis, we present techniques for more efficient learning and analysis of system behavior. The first part covers novel algorithms and tooling for testing systems based on active automata learning and Linear-time Temporal Logic (LTL) model checking, also called Learning-Based Testing (LBT). Next, we provide an improved learning algorithm that is able to deal with huge alphabets. These are commonly seen in large-scale industrial systems where input symbols contain data parameters.In the second part we discuss improvements for analyzing formal system specifications. We start out by looking at separated read, write and copy dependencies for symbolic model checking to speed up the verification of these specifications. Then, we show that bandwidth reduction techniques, originally designed for sparse matrix solvers, are very capable at reducing the memory footprint of the specifications' symbolic state space. Implementations of the presented algorithms are subjected to case studies and rigorous experimentation with scientific software competitions.

    U2 - 10.3990/1.9789036548441

    DO - 10.3990/1.9789036548441

    M3 - PhD Thesis - Research UT, graduation UT

    SN - 978-90-365-4844-1

    T3 - DSI Ph.D. thesis series

    PB - University of Twente

    CY - Enschede

    ER -

    Meijer J. Efficient learning and analysis of system behavior. Enschede: University of Twente, 2019. 201 p. (DSI Ph.D. thesis series; 19-015). (IPA Dissertation Series; 2019-10). https://doi.org/10.3990/1.9789036548441