An Efficient Model Inference Algorithm for Learning-based Testing of Reactive Systems

TL;DR

This paper introduces the IKL learning algorithm for deterministic Kripke structures, enhancing scalability in learning-based testing of reactive systems through formal correctness and optimization techniques.

Contribution

The paper presents the IKL algorithm, a novel active incremental learning method with proven correctness and scalability optimizations for model inference in testing reactive systems.

Findings

IKL algorithm is correct and formally verified.

Optimizations improve scalability for large systems.

Black box heuristic effectively determines test termination.

Abstract

Learning-based testing (LBT) is an emerging methodology to automate iterative black-box requirements testing of software systems. The methodology involves combining model inference with model checking techniques. However, a variety of optimisations on model inference are necessary in order to achieve scalable testing for large systems. In this paper we describe the IKL learning algorithm which is an active incremental learning algorithm for deterministic Kripke structures. We formally prove the correctness of IKL. We discuss the optimisations it incorporates to achieve scalability of testing. We also evaluate a black box heuristic for test termination based on convergence of IKL learning.