Efficient learning and analysis of system behavior

Jeroen Meijer

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

101 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 UTAcademic

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